begin
:: deftheorem Def1 defines inv1 GFACIRC1:def 1 :
theorem Th1:
:: deftheorem Def2 defines buf1 GFACIRC1:def 2 :
theorem
definition
func and2c -> Function of
(2 -tuples_on BOOLEAN ),
BOOLEAN means :
Def3:
for
x,
y being
Element of
BOOLEAN holds
it . <*x,y*> = x '&' ('not' y);
existence
ex b1 being Function of (2 -tuples_on BOOLEAN ),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x '&' ('not' 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 '&' ('not' y) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x '&' ('not' y) ) holds
b1 = b2
end;
:: deftheorem Def3 defines and2c GFACIRC1:def 3 :
theorem
for
x,
y being
Element of
BOOLEAN holds
(
and2c . <*x,y*> = x '&' ('not' y) &
and2c . <*x,y*> = and2a . <*y,x*> &
and2c . <*x,y*> = nor2a . <*x,y*> &
and2c . <*0 ,0 *> = 0 &
and2c . <*0 ,1*> = 0 &
and2c . <*1,0 *> = 1 &
and2c . <*1,1*> = 0 )
definition
func xor2c -> Function of
(2 -tuples_on BOOLEAN ),
BOOLEAN means :
Def4:
for
x,
y being
Element of
BOOLEAN holds
it . <*x,y*> = x 'xor' ('not' y);
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' ('not' 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' ('not' y) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x 'xor' ('not' y) ) holds
b1 = b2
end;
:: deftheorem Def4 defines xor2c GFACIRC1:def 4 :
theorem Th4:
for
x,
y being
Element of
BOOLEAN holds
(
xor2c . <*x,y*> = x 'xor' ('not' y) &
xor2c . <*x,y*> = xor2a . <*x,y*> &
xor2c . <*x,y*> = or2 . <*(and2b . <*x,y*>),(and2 . <*x,y*>)*> &
xor2c . <*0 ,0 *> = 1 &
xor2c . <*0 ,1*> = 0 &
xor2c . <*1,0 *> = 0 &
xor2c . <*1,1*> = 1 )
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
canceled;
theorem
Lm1:
for f1, f2, f3 being Function of (2 -tuples_on BOOLEAN ),BOOLEAN
for x, y, z being set st x <> [<*y,z*>,f2] & y <> [<*z,x*>,f3] & z <> [<*x,y*>,f1] holds
( not [<*x,y*>,f1] in {y,z} & not z in {[<*x,y*>,f1],[<*y,z*>,f2]} & not x in {[<*x,y*>,f1],[<*y,z*>,f2]} & not [<*z,x*>,f3] in {x,y,z} )
Lm2:
for f1, f2, f3 being Function of (2 -tuples_on BOOLEAN ),BOOLEAN
for f4 being Function of (3 -tuples_on BOOLEAN ),BOOLEAN
for x, y, z being set holds {x,y,z} \ {[<*[<*x,y*>,f1],[<*y,z*>,f2],[<*z,x*>,f3]*>,f4]} = {x,y,z}
Lm3:
for f being Function of (2 -tuples_on BOOLEAN ),BOOLEAN
for x, y, c being set st c <> [<*x,y*>,f] holds
for s being State of (2GatesCircuit x,y,c,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 )
begin
definition
let x,
y,
z be
set ;
func GFA0CarryIStr x,
y,
z -> non
empty non
void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals
((1GateCircStr <*x,y*>,and2 ) +* (1GateCircStr <*y,z*>,and2 )) +* (1GateCircStr <*z,x*>,and2 );
coherence
((1GateCircStr <*x,y*>,and2 ) +* (1GateCircStr <*y,z*>,and2 )) +* (1GateCircStr <*z,x*>,and2 ) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
;
end;
:: deftheorem defines GFA0CarryIStr GFACIRC1:def 5 :
for
x,
y,
z being
set holds
GFA0CarryIStr x,
y,
z = ((1GateCircStr <*x,y*>,and2 ) +* (1GateCircStr <*y,z*>,and2 )) +* (1GateCircStr <*z,x*>,and2 );
definition
let x,
y,
z be
set ;
func GFA0CarryICirc x,
y,
z -> strict gate`2=den Boolean Circuit of
GFA0CarryIStr x,
y,
z equals
((1GateCircuit x,y,and2 ) +* (1GateCircuit y,z,and2 )) +* (1GateCircuit z,x,and2 );
coherence
((1GateCircuit x,y,and2 ) +* (1GateCircuit y,z,and2 )) +* (1GateCircuit z,x,and2 ) is strict gate`2=den Boolean Circuit of GFA0CarryIStr x,y,z
;
end;
:: deftheorem defines GFA0CarryICirc GFACIRC1:def 6 :
for
x,
y,
z being
set holds
GFA0CarryICirc x,
y,
z = ((1GateCircuit x,y,and2 ) +* (1GateCircuit y,z,and2 )) +* (1GateCircuit z,x,and2 );
definition
let x,
y,
z be
set ;
func GFA0CarryStr x,
y,
z -> non
empty non
void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals
(GFA0CarryIStr x,y,z) +* (1GateCircStr <*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 );
coherence
(GFA0CarryIStr x,y,z) +* (1GateCircStr <*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 ) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
;
end;
:: deftheorem defines GFA0CarryStr GFACIRC1:def 7 :
for
x,
y,
z being
set holds
GFA0CarryStr x,
y,
z = (GFA0CarryIStr x,y,z) +* (1GateCircStr <*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 );
definition
let x,
y,
z be
set ;
func GFA0CarryCirc x,
y,
z -> strict gate`2=den Boolean Circuit of
GFA0CarryStr x,
y,
z equals
(GFA0CarryICirc x,y,z) +* (1GateCircuit [<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ],or3 );
coherence
(GFA0CarryICirc x,y,z) +* (1GateCircuit [<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ],or3 ) is strict gate`2=den Boolean Circuit of GFA0CarryStr x,y,z
;
end;
:: deftheorem defines GFA0CarryCirc GFACIRC1:def 8 :
for
x,
y,
z being
set holds
GFA0CarryCirc x,
y,
z = (GFA0CarryICirc x,y,z) +* (1GateCircuit [<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ],or3 );
definition
let x,
y,
z be
set ;
func GFA0CarryOutput x,
y,
z -> Element of
InnerVertices (GFA0CarryStr x,y,z) equals
[<*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 ];
coherence
[<*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 ] is Element of InnerVertices (GFA0CarryStr x,y,z)
end;
:: deftheorem defines GFA0CarryOutput GFACIRC1:def 9 :
for
x,
y,
z being
set holds
GFA0CarryOutput x,
y,
z = [<*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 ];
theorem Th13:
for
x,
y,
z being
set holds
InnerVertices (GFA0CarryIStr x,y,z) = {[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]}
theorem Th14:
for
x,
y,
z being
set holds
InnerVertices (GFA0CarryStr x,y,z) = {[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]} \/ {(GFA0CarryOutput x,y,z)}
theorem Th15:
theorem Th16:
for
x,
y,
z being
set st
x <> [<*y,z*>,and2 ] &
y <> [<*z,x*>,and2 ] &
z <> [<*x,y*>,and2 ] holds
InputVertices (GFA0CarryIStr x,y,z) = {x,y,z}
theorem Th17:
for
x,
y,
z being
set st
x <> [<*y,z*>,and2 ] &
y <> [<*z,x*>,and2 ] &
z <> [<*x,y*>,and2 ] holds
InputVertices (GFA0CarryStr x,y,z) = {x,y,z}
theorem
theorem Th19:
for
x,
y,
z being
set holds
(
x in the
carrier of
(GFA0CarryStr x,y,z) &
y in the
carrier of
(GFA0CarryStr x,y,z) &
z in the
carrier of
(GFA0CarryStr x,y,z) &
[<*x,y*>,and2 ] in the
carrier of
(GFA0CarryStr x,y,z) &
[<*y,z*>,and2 ] in the
carrier of
(GFA0CarryStr x,y,z) &
[<*z,x*>,and2 ] in the
carrier of
(GFA0CarryStr x,y,z) &
[<*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 ] in the
carrier of
(GFA0CarryStr x,y,z) )
theorem Th20:
for
x,
y,
z being
set holds
(
[<*x,y*>,and2 ] in InnerVertices (GFA0CarryStr x,y,z) &
[<*y,z*>,and2 ] in InnerVertices (GFA0CarryStr x,y,z) &
[<*z,x*>,and2 ] in InnerVertices (GFA0CarryStr x,y,z) &
GFA0CarryOutput x,
y,
z in InnerVertices (GFA0CarryStr x,y,z) )
theorem Th21:
for
x,
y,
z being
set st
x <> [<*y,z*>,and2 ] &
y <> [<*z,x*>,and2 ] &
z <> [<*x,y*>,and2 ] holds
(
x in InputVertices (GFA0CarryStr x,y,z) &
y in InputVertices (GFA0CarryStr x,y,z) &
z in InputVertices (GFA0CarryStr x,y,z) )
theorem Th22:
theorem Th23:
for
x,
y,
z being
set for
s being
State of
(GFA0CarryCirc x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . z holds
(
(Following s) . [<*x,y*>,and2 ] = a1 '&' a2 &
(Following s) . [<*y,z*>,and2 ] = a2 '&' a3 &
(Following s) . [<*z,x*>,and2 ] = a3 '&' a1 )
theorem Th24:
for
x,
y,
z being
set for
s being
State of
(GFA0CarryCirc x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . [<*x,y*>,and2 ] &
a2 = s . [<*y,z*>,and2 ] &
a3 = s . [<*z,x*>,and2 ] holds
(Following s) . (GFA0CarryOutput x,y,z) = (a1 'or' a2) 'or' a3
theorem Th25:
for
x,
y,
z being
set st
x <> [<*y,z*>,and2 ] &
y <> [<*z,x*>,and2 ] &
z <> [<*x,y*>,and2 ] holds
for
s being
State of
(GFA0CarryCirc x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . z holds
(
(Following s,2) . (GFA0CarryOutput x,y,z) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) &
(Following s,2) . [<*x,y*>,and2 ] = a1 '&' a2 &
(Following s,2) . [<*y,z*>,and2 ] = a2 '&' a3 &
(Following s,2) . [<*z,x*>,and2 ] = a3 '&' a1 )
theorem Th26:
for
x,
y,
z being
set st
x <> [<*y,z*>,and2 ] &
y <> [<*z,x*>,and2 ] &
z <> [<*x,y*>,and2 ] holds
for
s being
State of
(GFA0CarryCirc x,y,z) holds
Following s,2 is
stable
definition
let x,
y,
z be
set ;
func GFA0AdderStr x,
y,
z -> non
empty non
void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals
2GatesCircStr x,
y,
z,
xor2 ;
coherence
2GatesCircStr x,y,z,xor2 is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
;
end;
:: deftheorem defines GFA0AdderStr GFACIRC1:def 10 :
definition
let x,
y,
z be
set ;
func GFA0AdderCirc x,
y,
z -> strict gate`2=den Boolean Circuit of
GFA0AdderStr x,
y,
z equals
2GatesCircuit x,
y,
z,
xor2 ;
coherence
2GatesCircuit x,y,z,xor2 is strict gate`2=den Boolean Circuit of GFA0AdderStr x,y,z
;
end;
:: deftheorem defines GFA0AdderCirc GFACIRC1:def 11 :
definition
let x,
y,
z be
set ;
func GFA0AdderOutput x,
y,
z -> Element of
InnerVertices (GFA0AdderStr x,y,z) equals
2GatesCircOutput x,
y,
z,
xor2 ;
coherence
2GatesCircOutput x,y,z,xor2 is Element of InnerVertices (GFA0AdderStr x,y,z)
;
end;
:: deftheorem defines GFA0AdderOutput GFACIRC1:def 12 :
theorem Th27:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
for
x,
y,
z being
set holds
(
x in the
carrier of
(GFA0AdderStr x,y,z) &
y in the
carrier of
(GFA0AdderStr x,y,z) &
z in the
carrier of
(GFA0AdderStr x,y,z) &
[<*x,y*>,xor2 ] in the
carrier of
(GFA0AdderStr x,y,z) &
[<*[<*x,y*>,xor2 ],z*>,xor2 ] in the
carrier of
(GFA0AdderStr x,y,z) )
by FACIRC_1:60, FACIRC_1:61;
theorem Th32:
for
x,
y,
z being
set holds
(
[<*x,y*>,xor2 ] in InnerVertices (GFA0AdderStr x,y,z) &
GFA0AdderOutput x,
y,
z in InnerVertices (GFA0AdderStr x,y,z) )
theorem Th33:
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2 ] holds
(
x in InputVertices (GFA0AdderStr x,y,z) &
y in InputVertices (GFA0AdderStr x,y,z) &
z in InputVertices (GFA0AdderStr x,y,z) )
theorem
canceled;
theorem Th35:
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2 ] holds
for
s being
State of
(GFA0AdderCirc x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . z holds
(
(Following s) . [<*x,y*>,xor2 ] = a1 'xor' a2 &
(Following s) . x = a1 &
(Following s) . y = a2 &
(Following s) . z = a3 )
theorem Th36:
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2 ] holds
for
s being
State of
(GFA0AdderCirc x,y,z) for
a1a2,
a1,
a2,
a3 being
Element of
BOOLEAN st
a1a2 = s . [<*x,y*>,xor2 ] &
a3 = s . z holds
(Following s) . (GFA0AdderOutput x,y,z) = a1a2 'xor' a3
theorem Th37:
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2 ] holds
for
s being
State of
(GFA0AdderCirc x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . z holds
(
(Following s,2) . (GFA0AdderOutput x,y,z) = (a1 'xor' a2) 'xor' a3 &
(Following s,2) . [<*x,y*>,xor2 ] = a1 'xor' a2 &
(Following s,2) . x = a1 &
(Following s,2) . y = a2 &
(Following s,2) . z = a3 )
definition
let x,
y,
z be
set ;
func BitGFA0Str x,
y,
z -> non
empty non
void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals
(GFA0AdderStr x,y,z) +* (GFA0CarryStr x,y,z);
coherence
(GFA0AdderStr x,y,z) +* (GFA0CarryStr x,y,z) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
;
end;
:: deftheorem defines BitGFA0Str GFACIRC1:def 13 :
definition
let x,
y,
z be
set ;
func BitGFA0Circ x,
y,
z -> strict gate`2=den Boolean Circuit of
BitGFA0Str x,
y,
z equals
(GFA0AdderCirc x,y,z) +* (GFA0CarryCirc x,y,z);
coherence
(GFA0AdderCirc x,y,z) +* (GFA0CarryCirc x,y,z) is strict gate`2=den Boolean Circuit of BitGFA0Str x,y,z
;
end;
:: deftheorem defines BitGFA0Circ GFACIRC1:def 14 :
theorem
canceled;
theorem Th39:
for
x,
y,
z being
set holds
InnerVertices (BitGFA0Str x,y,z) = (({[<*x,y*>,xor2 ]} \/ {(GFA0AdderOutput x,y,z)}) \/ {[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]}) \/ {(GFA0CarryOutput x,y,z)}
theorem
theorem Th41:
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2 ] &
x <> [<*y,z*>,and2 ] &
y <> [<*z,x*>,and2 ] &
z <> [<*x,y*>,and2 ] holds
InputVertices (BitGFA0Str x,y,z) = {x,y,z}
theorem Th42:
theorem
theorem
for
x,
y,
z being
set holds
(
x in the
carrier of
(BitGFA0Str x,y,z) &
y in the
carrier of
(BitGFA0Str x,y,z) &
z in the
carrier of
(BitGFA0Str x,y,z) &
[<*x,y*>,xor2 ] in the
carrier of
(BitGFA0Str x,y,z) &
[<*[<*x,y*>,xor2 ],z*>,xor2 ] in the
carrier of
(BitGFA0Str x,y,z) &
[<*x,y*>,and2 ] in the
carrier of
(BitGFA0Str x,y,z) &
[<*y,z*>,and2 ] in the
carrier of
(BitGFA0Str x,y,z) &
[<*z,x*>,and2 ] in the
carrier of
(BitGFA0Str x,y,z) &
[<*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 ] in the
carrier of
(BitGFA0Str x,y,z) )
theorem Th45:
for
x,
y,
z being
set holds
(
[<*x,y*>,xor2 ] in InnerVertices (BitGFA0Str x,y,z) &
GFA0AdderOutput x,
y,
z in InnerVertices (BitGFA0Str x,y,z) &
[<*x,y*>,and2 ] in InnerVertices (BitGFA0Str x,y,z) &
[<*y,z*>,and2 ] in InnerVertices (BitGFA0Str x,y,z) &
[<*z,x*>,and2 ] in InnerVertices (BitGFA0Str x,y,z) &
GFA0CarryOutput x,
y,
z in InnerVertices (BitGFA0Str x,y,z) )
theorem
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2 ] &
x <> [<*y,z*>,and2 ] &
y <> [<*z,x*>,and2 ] &
z <> [<*x,y*>,and2 ] holds
(
x in InputVertices (BitGFA0Str x,y,z) &
y in InputVertices (BitGFA0Str x,y,z) &
z in InputVertices (BitGFA0Str x,y,z) )
definition
let x,
y,
z be
set ;
func BitGFA0CarryOutput x,
y,
z -> Element of
InnerVertices (BitGFA0Str x,y,z) equals
[<*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 ];
coherence
[<*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 ] is Element of InnerVertices (BitGFA0Str x,y,z)
end;
:: deftheorem defines BitGFA0CarryOutput GFACIRC1:def 15 :
for
x,
y,
z being
set holds
BitGFA0CarryOutput x,
y,
z = [<*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 ];
definition
let x,
y,
z be
set ;
func BitGFA0AdderOutput x,
y,
z -> Element of
InnerVertices (BitGFA0Str x,y,z) equals
2GatesCircOutput x,
y,
z,
xor2 ;
coherence
2GatesCircOutput x,y,z,xor2 is Element of InnerVertices (BitGFA0Str x,y,z)
end;
:: deftheorem defines BitGFA0AdderOutput GFACIRC1:def 16 :
theorem
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2 ] &
x <> [<*y,z*>,and2 ] &
y <> [<*z,x*>,and2 ] &
z <> [<*x,y*>,and2 ] holds
for
s being
State of
(BitGFA0Circ x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . z holds
(
(Following s,2) . (GFA0AdderOutput x,y,z) = (a1 'xor' a2) 'xor' a3 &
(Following s,2) . (GFA0CarryOutput x,y,z) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) )
theorem
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2 ] &
x <> [<*y,z*>,and2 ] &
y <> [<*z,x*>,and2 ] &
z <> [<*x,y*>,and2 ] holds
for
s being
State of
(BitGFA0Circ x,y,z) holds
Following s,2 is
stable
begin
definition
let x,
y,
z be
set ;
func GFA1CarryIStr x,
y,
z -> non
empty non
void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals
((1GateCircStr <*x,y*>,and2c ) +* (1GateCircStr <*y,z*>,and2a )) +* (1GateCircStr <*z,x*>,and2 );
coherence
((1GateCircStr <*x,y*>,and2c ) +* (1GateCircStr <*y,z*>,and2a )) +* (1GateCircStr <*z,x*>,and2 ) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
;
end;
:: deftheorem defines GFA1CarryIStr GFACIRC1:def 17 :
for
x,
y,
z being
set holds
GFA1CarryIStr x,
y,
z = ((1GateCircStr <*x,y*>,and2c ) +* (1GateCircStr <*y,z*>,and2a )) +* (1GateCircStr <*z,x*>,and2 );
definition
let x,
y,
z be
set ;
func GFA1CarryICirc x,
y,
z -> strict gate`2=den Boolean Circuit of
GFA1CarryIStr x,
y,
z equals
((1GateCircuit x,y,and2c ) +* (1GateCircuit y,z,and2a )) +* (1GateCircuit z,x,and2 );
coherence
((1GateCircuit x,y,and2c ) +* (1GateCircuit y,z,and2a )) +* (1GateCircuit z,x,and2 ) is strict gate`2=den Boolean Circuit of GFA1CarryIStr x,y,z
;
end;
:: deftheorem defines GFA1CarryICirc GFACIRC1:def 18 :
for
x,
y,
z being
set holds
GFA1CarryICirc x,
y,
z = ((1GateCircuit x,y,and2c ) +* (1GateCircuit y,z,and2a )) +* (1GateCircuit z,x,and2 );
definition
let x,
y,
z be
set ;
func GFA1CarryStr x,
y,
z -> non
empty non
void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals
(GFA1CarryIStr x,y,z) +* (1GateCircStr <*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 );
coherence
(GFA1CarryIStr x,y,z) +* (1GateCircStr <*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
;
end;
:: deftheorem defines GFA1CarryStr GFACIRC1:def 19 :
for
x,
y,
z being
set holds
GFA1CarryStr x,
y,
z = (GFA1CarryIStr x,y,z) +* (1GateCircStr <*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 );
definition
let x,
y,
z be
set ;
func GFA1CarryCirc x,
y,
z -> strict gate`2=den Boolean Circuit of
GFA1CarryStr x,
y,
z equals
(GFA1CarryICirc x,y,z) +* (1GateCircuit [<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ],or3 );
coherence
(GFA1CarryICirc x,y,z) +* (1GateCircuit [<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ],or3 ) is strict gate`2=den Boolean Circuit of GFA1CarryStr x,y,z
;
end;
:: deftheorem defines GFA1CarryCirc GFACIRC1:def 20 :
for
x,
y,
z being
set holds
GFA1CarryCirc x,
y,
z = (GFA1CarryICirc x,y,z) +* (1GateCircuit [<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ],or3 );
definition
let x,
y,
z be
set ;
func GFA1CarryOutput x,
y,
z -> Element of
InnerVertices (GFA1CarryStr x,y,z) equals
[<*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ];
coherence
[<*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ] is Element of InnerVertices (GFA1CarryStr x,y,z)
end;
:: deftheorem defines GFA1CarryOutput GFACIRC1:def 21 :
for
x,
y,
z being
set holds
GFA1CarryOutput x,
y,
z = [<*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ];
theorem Th49:
for
x,
y,
z being
set holds
InnerVertices (GFA1CarryIStr x,y,z) = {[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]}
theorem Th50:
for
x,
y,
z being
set holds
InnerVertices (GFA1CarryStr x,y,z) = {[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]} \/ {(GFA1CarryOutput x,y,z)}
theorem Th51:
theorem Th52:
for
x,
y,
z being
set st
x <> [<*y,z*>,and2a ] &
y <> [<*z,x*>,and2 ] &
z <> [<*x,y*>,and2c ] holds
InputVertices (GFA1CarryIStr x,y,z) = {x,y,z}
theorem Th53:
for
x,
y,
z being
set st
x <> [<*y,z*>,and2a ] &
y <> [<*z,x*>,and2 ] &
z <> [<*x,y*>,and2c ] holds
InputVertices (GFA1CarryStr x,y,z) = {x,y,z}
theorem
theorem Th55:
for
x,
y,
z being
set holds
(
x in the
carrier of
(GFA1CarryStr x,y,z) &
y in the
carrier of
(GFA1CarryStr x,y,z) &
z in the
carrier of
(GFA1CarryStr x,y,z) &
[<*x,y*>,and2c ] in the
carrier of
(GFA1CarryStr x,y,z) &
[<*y,z*>,and2a ] in the
carrier of
(GFA1CarryStr x,y,z) &
[<*z,x*>,and2 ] in the
carrier of
(GFA1CarryStr x,y,z) &
[<*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ] in the
carrier of
(GFA1CarryStr x,y,z) )
theorem Th56:
for
x,
y,
z being
set holds
(
[<*x,y*>,and2c ] in InnerVertices (GFA1CarryStr x,y,z) &
[<*y,z*>,and2a ] in InnerVertices (GFA1CarryStr x,y,z) &
[<*z,x*>,and2 ] in InnerVertices (GFA1CarryStr x,y,z) &
GFA1CarryOutput x,
y,
z in InnerVertices (GFA1CarryStr x,y,z) )
theorem Th57:
for
x,
y,
z being
set st
x <> [<*y,z*>,and2a ] &
y <> [<*z,x*>,and2 ] &
z <> [<*x,y*>,and2c ] holds
(
x in InputVertices (GFA1CarryStr x,y,z) &
y in InputVertices (GFA1CarryStr x,y,z) &
z in InputVertices (GFA1CarryStr x,y,z) )
theorem Th58:
theorem Th59:
for
x,
y,
z being
set for
s being
State of
(GFA1CarryCirc x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . z holds
(
(Following s) . [<*x,y*>,and2c ] = a1 '&' ('not' a2) &
(Following s) . [<*y,z*>,and2a ] = ('not' a2) '&' a3 &
(Following s) . [<*z,x*>,and2 ] = a3 '&' a1 )
theorem Th60:
for
x,
y,
z being
set for
s being
State of
(GFA1CarryCirc x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . [<*x,y*>,and2c ] &
a2 = s . [<*y,z*>,and2a ] &
a3 = s . [<*z,x*>,and2 ] holds
(Following s) . (GFA1CarryOutput x,y,z) = (a1 'or' a2) 'or' a3
theorem Th61:
for
x,
y,
z being
set st
x <> [<*y,z*>,and2a ] &
y <> [<*z,x*>,and2 ] &
z <> [<*x,y*>,and2c ] holds
for
s being
State of
(GFA1CarryCirc x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . z holds
(
(Following s,2) . (GFA1CarryOutput x,y,z) = ((a1 '&' ('not' a2)) 'or' (('not' a2) '&' a3)) 'or' (a3 '&' a1) &
(Following s,2) . [<*x,y*>,and2c ] = a1 '&' ('not' a2) &
(Following s,2) . [<*y,z*>,and2a ] = ('not' a2) '&' a3 &
(Following s,2) . [<*z,x*>,and2 ] = a3 '&' a1 )
theorem Th62:
for
x,
y,
z being
set st
x <> [<*y,z*>,and2a ] &
y <> [<*z,x*>,and2 ] &
z <> [<*x,y*>,and2c ] holds
for
s being
State of
(GFA1CarryCirc x,y,z) holds
Following s,2 is
stable
definition
let x,
y,
z be
set ;
func GFA1AdderStr x,
y,
z -> non
empty non
void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals
2GatesCircStr x,
y,
z,
xor2c ;
coherence
2GatesCircStr x,y,z,xor2c is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
;
end;
:: deftheorem defines GFA1AdderStr GFACIRC1:def 22 :
definition
let x,
y,
z be
set ;
func GFA1AdderCirc x,
y,
z -> strict gate`2=den Boolean Circuit of
GFA1AdderStr x,
y,
z equals
2GatesCircuit x,
y,
z,
xor2c ;
coherence
2GatesCircuit x,y,z,xor2c is strict gate`2=den Boolean Circuit of GFA1AdderStr x,y,z
;
end;
:: deftheorem defines GFA1AdderCirc GFACIRC1:def 23 :
definition
let x,
y,
z be
set ;
func GFA1AdderOutput x,
y,
z -> Element of
InnerVertices (GFA1AdderStr x,y,z) equals
2GatesCircOutput x,
y,
z,
xor2c ;
coherence
2GatesCircOutput x,y,z,xor2c is Element of InnerVertices (GFA1AdderStr x,y,z)
;
end;
:: deftheorem defines GFA1AdderOutput GFACIRC1:def 24 :
theorem Th63:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
for
x,
y,
z being
set holds
(
x in the
carrier of
(GFA1AdderStr x,y,z) &
y in the
carrier of
(GFA1AdderStr x,y,z) &
z in the
carrier of
(GFA1AdderStr x,y,z) &
[<*x,y*>,xor2c ] in the
carrier of
(GFA1AdderStr x,y,z) &
[<*[<*x,y*>,xor2c ],z*>,xor2c ] in the
carrier of
(GFA1AdderStr x,y,z) )
by FACIRC_1:60, FACIRC_1:61;
theorem Th68:
for
x,
y,
z being
set holds
(
[<*x,y*>,xor2c ] in InnerVertices (GFA1AdderStr x,y,z) &
GFA1AdderOutput x,
y,
z in InnerVertices (GFA1AdderStr x,y,z) )
theorem Th69:
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2c ] holds
(
x in InputVertices (GFA1AdderStr x,y,z) &
y in InputVertices (GFA1AdderStr x,y,z) &
z in InputVertices (GFA1AdderStr x,y,z) )
theorem
canceled;
theorem Th71:
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2c ] holds
for
s being
State of
(GFA1AdderCirc x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . z holds
(
(Following s) . [<*x,y*>,xor2c ] = a1 'xor' ('not' a2) &
(Following s) . x = a1 &
(Following s) . y = a2 &
(Following s) . z = a3 )
theorem Th72:
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2c ] holds
for
s being
State of
(GFA1AdderCirc x,y,z) for
a1a2,
a1,
a2,
a3 being
Element of
BOOLEAN st
a1a2 = s . [<*x,y*>,xor2c ] &
a3 = s . z holds
(Following s) . (GFA1AdderOutput x,y,z) = a1a2 'xor' ('not' a3)
theorem Th73:
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2c ] holds
for
s being
State of
(GFA1AdderCirc x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . z holds
(
(Following s,2) . (GFA1AdderOutput x,y,z) = (a1 'xor' ('not' a2)) 'xor' ('not' a3) &
(Following s,2) . [<*x,y*>,xor2c ] = a1 'xor' ('not' a2) &
(Following s,2) . x = a1 &
(Following s,2) . y = a2 &
(Following s,2) . z = a3 )
theorem Th74:
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2c ] holds
for
s being
State of
(GFA1AdderCirc x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . z holds
(Following s,2) . (GFA1AdderOutput x,y,z) = 'not' ((a1 'xor' ('not' a2)) 'xor' a3)
definition
let x,
y,
z be
set ;
func BitGFA1Str x,
y,
z -> non
empty non
void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals
(GFA1AdderStr x,y,z) +* (GFA1CarryStr x,y,z);
coherence
(GFA1AdderStr x,y,z) +* (GFA1CarryStr x,y,z) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
;
end;
:: deftheorem defines BitGFA1Str GFACIRC1:def 25 :
definition
let x,
y,
z be
set ;
func BitGFA1Circ x,
y,
z -> strict gate`2=den Boolean Circuit of
BitGFA1Str x,
y,
z equals
(GFA1AdderCirc x,y,z) +* (GFA1CarryCirc x,y,z);
coherence
(GFA1AdderCirc x,y,z) +* (GFA1CarryCirc x,y,z) is strict gate`2=den Boolean Circuit of BitGFA1Str x,y,z
;
end;
:: deftheorem defines BitGFA1Circ GFACIRC1:def 26 :
theorem
canceled;
theorem Th76:
for
x,
y,
z being
set holds
InnerVertices (BitGFA1Str x,y,z) = (({[<*x,y*>,xor2c ]} \/ {(GFA1AdderOutput x,y,z)}) \/ {[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]}) \/ {(GFA1CarryOutput x,y,z)}
theorem
theorem Th78:
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2c ] &
x <> [<*y,z*>,and2a ] &
y <> [<*z,x*>,and2 ] &
z <> [<*x,y*>,and2c ] holds
InputVertices (BitGFA1Str x,y,z) = {x,y,z}
theorem Th79:
theorem
theorem
for
x,
y,
z being
set holds
(
x in the
carrier of
(BitGFA1Str x,y,z) &
y in the
carrier of
(BitGFA1Str x,y,z) &
z in the
carrier of
(BitGFA1Str x,y,z) &
[<*x,y*>,xor2c ] in the
carrier of
(BitGFA1Str x,y,z) &
[<*[<*x,y*>,xor2c ],z*>,xor2c ] in the
carrier of
(BitGFA1Str x,y,z) &
[<*x,y*>,and2c ] in the
carrier of
(BitGFA1Str x,y,z) &
[<*y,z*>,and2a ] in the
carrier of
(BitGFA1Str x,y,z) &
[<*z,x*>,and2 ] in the
carrier of
(BitGFA1Str x,y,z) &
[<*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ] in the
carrier of
(BitGFA1Str x,y,z) )
theorem Th82:
for
x,
y,
z being
set holds
(
[<*x,y*>,xor2c ] in InnerVertices (BitGFA1Str x,y,z) &
GFA1AdderOutput x,
y,
z in InnerVertices (BitGFA1Str x,y,z) &
[<*x,y*>,and2c ] in InnerVertices (BitGFA1Str x,y,z) &
[<*y,z*>,and2a ] in InnerVertices (BitGFA1Str x,y,z) &
[<*z,x*>,and2 ] in InnerVertices (BitGFA1Str x,y,z) &
GFA1CarryOutput x,
y,
z in InnerVertices (BitGFA1Str x,y,z) )
theorem
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2c ] &
x <> [<*y,z*>,and2a ] &
y <> [<*z,x*>,and2 ] &
z <> [<*x,y*>,and2c ] holds
(
x in InputVertices (BitGFA1Str x,y,z) &
y in InputVertices (BitGFA1Str x,y,z) &
z in InputVertices (BitGFA1Str x,y,z) )
definition
let x,
y,
z be
set ;
func BitGFA1CarryOutput x,
y,
z -> Element of
InnerVertices (BitGFA1Str x,y,z) equals
[<*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ];
coherence
[<*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ] is Element of InnerVertices (BitGFA1Str x,y,z)
end;
:: deftheorem defines BitGFA1CarryOutput GFACIRC1:def 27 :
for
x,
y,
z being
set holds
BitGFA1CarryOutput x,
y,
z = [<*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ];
definition
let x,
y,
z be
set ;
func BitGFA1AdderOutput x,
y,
z -> Element of
InnerVertices (BitGFA1Str x,y,z) equals
2GatesCircOutput x,
y,
z,
xor2c ;
coherence
2GatesCircOutput x,y,z,xor2c is Element of InnerVertices (BitGFA1Str x,y,z)
end;
:: deftheorem defines BitGFA1AdderOutput GFACIRC1:def 28 :
theorem
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2c ] &
x <> [<*y,z*>,and2a ] &
y <> [<*z,x*>,and2 ] &
z <> [<*x,y*>,and2c ] holds
for
s being
State of
(BitGFA1Circ x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . z holds
(
(Following s,2) . (GFA1AdderOutput x,y,z) = 'not' ((a1 'xor' ('not' a2)) 'xor' a3) &
(Following s,2) . (GFA1CarryOutput x,y,z) = ((a1 '&' ('not' a2)) 'or' (('not' a2) '&' a3)) 'or' (a3 '&' a1) )
theorem
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2c ] &
x <> [<*y,z*>,and2a ] &
y <> [<*z,x*>,and2 ] &
z <> [<*x,y*>,and2c ] holds
for
s being
State of
(BitGFA1Circ x,y,z) holds
Following s,2 is
stable
begin
definition
let x,
y,
z be
set ;
func GFA2CarryIStr x,
y,
z -> non
empty non
void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals
((1GateCircStr <*x,y*>,and2a ) +* (1GateCircStr <*y,z*>,and2c )) +* (1GateCircStr <*z,x*>,and2b );
coherence
((1GateCircStr <*x,y*>,and2a ) +* (1GateCircStr <*y,z*>,and2c )) +* (1GateCircStr <*z,x*>,and2b ) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
;
end;
:: deftheorem defines GFA2CarryIStr GFACIRC1:def 29 :
for
x,
y,
z being
set holds
GFA2CarryIStr x,
y,
z = ((1GateCircStr <*x,y*>,and2a ) +* (1GateCircStr <*y,z*>,and2c )) +* (1GateCircStr <*z,x*>,and2b );
definition
let x,
y,
z be
set ;
func GFA2CarryICirc x,
y,
z -> strict gate`2=den Boolean Circuit of
GFA2CarryIStr x,
y,
z equals
((1GateCircuit x,y,and2a ) +* (1GateCircuit y,z,and2c )) +* (1GateCircuit z,x,and2b );
coherence
((1GateCircuit x,y,and2a ) +* (1GateCircuit y,z,and2c )) +* (1GateCircuit z,x,and2b ) is strict gate`2=den Boolean Circuit of GFA2CarryIStr x,y,z
;
end;
:: deftheorem defines GFA2CarryICirc GFACIRC1:def 30 :
for
x,
y,
z being
set holds
GFA2CarryICirc x,
y,
z = ((1GateCircuit x,y,and2a ) +* (1GateCircuit y,z,and2c )) +* (1GateCircuit z,x,and2b );
definition
let x,
y,
z be
set ;
func GFA2CarryStr x,
y,
z -> non
empty non
void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals
(GFA2CarryIStr x,y,z) +* (1GateCircStr <*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 );
coherence
(GFA2CarryIStr x,y,z) +* (1GateCircStr <*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 ) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
;
end;
:: deftheorem defines GFA2CarryStr GFACIRC1:def 31 :
for
x,
y,
z being
set holds
GFA2CarryStr x,
y,
z = (GFA2CarryIStr x,y,z) +* (1GateCircStr <*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 );
definition
let x,
y,
z be
set ;
func GFA2CarryCirc x,
y,
z -> strict gate`2=den Boolean Circuit of
GFA2CarryStr x,
y,
z equals
(GFA2CarryICirc x,y,z) +* (1GateCircuit [<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ],nor3 );
coherence
(GFA2CarryICirc x,y,z) +* (1GateCircuit [<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ],nor3 ) is strict gate`2=den Boolean Circuit of GFA2CarryStr x,y,z
;
end;
:: deftheorem defines GFA2CarryCirc GFACIRC1:def 32 :
for
x,
y,
z being
set holds
GFA2CarryCirc x,
y,
z = (GFA2CarryICirc x,y,z) +* (1GateCircuit [<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ],nor3 );
definition
let x,
y,
z be
set ;
func GFA2CarryOutput x,
y,
z -> Element of
InnerVertices (GFA2CarryStr x,y,z) equals
[<*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 ];
coherence
[<*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 ] is Element of InnerVertices (GFA2CarryStr x,y,z)
end;
:: deftheorem defines GFA2CarryOutput GFACIRC1:def 33 :
for
x,
y,
z being
set holds
GFA2CarryOutput x,
y,
z = [<*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 ];
theorem Th86:
for
x,
y,
z being
set holds
InnerVertices (GFA2CarryIStr x,y,z) = {[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]}
theorem Th87:
for
x,
y,
z being
set holds
InnerVertices (GFA2CarryStr x,y,z) = {[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]} \/ {(GFA2CarryOutput x,y,z)}
theorem Th88:
theorem Th89:
for
x,
y,
z being
set st
x <> [<*y,z*>,and2c ] &
y <> [<*z,x*>,and2b ] &
z <> [<*x,y*>,and2a ] holds
InputVertices (GFA2CarryIStr x,y,z) = {x,y,z}
theorem Th90:
for
x,
y,
z being
set st
x <> [<*y,z*>,and2c ] &
y <> [<*z,x*>,and2b ] &
z <> [<*x,y*>,and2a ] holds
InputVertices (GFA2CarryStr x,y,z) = {x,y,z}
theorem
theorem Th92:
for
x,
y,
z being
set holds
(
x in the
carrier of
(GFA2CarryStr x,y,z) &
y in the
carrier of
(GFA2CarryStr x,y,z) &
z in the
carrier of
(GFA2CarryStr x,y,z) &
[<*x,y*>,and2a ] in the
carrier of
(GFA2CarryStr x,y,z) &
[<*y,z*>,and2c ] in the
carrier of
(GFA2CarryStr x,y,z) &
[<*z,x*>,and2b ] in the
carrier of
(GFA2CarryStr x,y,z) &
[<*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 ] in the
carrier of
(GFA2CarryStr x,y,z) )
theorem Th93:
for
x,
y,
z being
set holds
(
[<*x,y*>,and2a ] in InnerVertices (GFA2CarryStr x,y,z) &
[<*y,z*>,and2c ] in InnerVertices (GFA2CarryStr x,y,z) &
[<*z,x*>,and2b ] in InnerVertices (GFA2CarryStr x,y,z) &
GFA2CarryOutput x,
y,
z in InnerVertices (GFA2CarryStr x,y,z) )
theorem Th94:
for
x,
y,
z being
set st
x <> [<*y,z*>,and2c ] &
y <> [<*z,x*>,and2b ] &
z <> [<*x,y*>,and2a ] holds
(
x in InputVertices (GFA2CarryStr x,y,z) &
y in InputVertices (GFA2CarryStr x,y,z) &
z in InputVertices (GFA2CarryStr x,y,z) )
theorem Th95:
theorem Th96:
for
x,
y,
z being
set for
s being
State of
(GFA2CarryCirc x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . z holds
(
(Following s) . [<*x,y*>,and2a ] = ('not' a1) '&' a2 &
(Following s) . [<*y,z*>,and2c ] = a2 '&' ('not' a3) &
(Following s) . [<*z,x*>,and2b ] = ('not' a3) '&' ('not' a1) )
theorem Th97:
for
x,
y,
z being
set for
s being
State of
(GFA2CarryCirc x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . [<*x,y*>,and2a ] &
a2 = s . [<*y,z*>,and2c ] &
a3 = s . [<*z,x*>,and2b ] holds
(Following s) . (GFA2CarryOutput x,y,z) = 'not' ((a1 'or' a2) 'or' a3)
theorem Th98:
for
x,
y,
z being
set st
x <> [<*y,z*>,and2c ] &
y <> [<*z,x*>,and2b ] &
z <> [<*x,y*>,and2a ] holds
for
s being
State of
(GFA2CarryCirc x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . z holds
(
(Following s,2) . (GFA2CarryOutput x,y,z) = 'not' (((('not' a1) '&' a2) 'or' (a2 '&' ('not' a3))) 'or' (('not' a3) '&' ('not' a1))) &
(Following s,2) . [<*x,y*>,and2a ] = ('not' a1) '&' a2 &
(Following s,2) . [<*y,z*>,and2c ] = a2 '&' ('not' a3) &
(Following s,2) . [<*z,x*>,and2b ] = ('not' a3) '&' ('not' a1) )
theorem Th99:
for
x,
y,
z being
set st
x <> [<*y,z*>,and2c ] &
y <> [<*z,x*>,and2b ] &
z <> [<*x,y*>,and2a ] holds
for
s being
State of
(GFA2CarryCirc x,y,z) holds
Following s,2 is
stable
definition
let x,
y,
z be
set ;
func GFA2AdderStr x,
y,
z -> non
empty non
void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals
2GatesCircStr x,
y,
z,
xor2c ;
coherence
2GatesCircStr x,y,z,xor2c is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
;
end;
:: deftheorem defines GFA2AdderStr GFACIRC1:def 34 :
definition
let x,
y,
z be
set ;
func GFA2AdderCirc x,
y,
z -> strict gate`2=den Boolean Circuit of
GFA2AdderStr x,
y,
z equals
2GatesCircuit x,
y,
z,
xor2c ;
coherence
2GatesCircuit x,y,z,xor2c is strict gate`2=den Boolean Circuit of GFA2AdderStr x,y,z
;
end;
:: deftheorem defines GFA2AdderCirc GFACIRC1:def 35 :
definition
let x,
y,
z be
set ;
func GFA2AdderOutput x,
y,
z -> Element of
InnerVertices (GFA2AdderStr x,y,z) equals
2GatesCircOutput x,
y,
z,
xor2c ;
coherence
2GatesCircOutput x,y,z,xor2c is Element of InnerVertices (GFA2AdderStr x,y,z)
;
end;
:: deftheorem defines GFA2AdderOutput GFACIRC1:def 36 :
theorem Th100:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
for
x,
y,
z being
set holds
(
x in the
carrier of
(GFA2AdderStr x,y,z) &
y in the
carrier of
(GFA2AdderStr x,y,z) &
z in the
carrier of
(GFA2AdderStr x,y,z) &
[<*x,y*>,xor2c ] in the
carrier of
(GFA2AdderStr x,y,z) &
[<*[<*x,y*>,xor2c ],z*>,xor2c ] in the
carrier of
(GFA2AdderStr x,y,z) )
by FACIRC_1:60, FACIRC_1:61;
theorem
for
x,
y,
z being
set holds
(
[<*x,y*>,xor2c ] in InnerVertices (GFA2AdderStr x,y,z) &
GFA2AdderOutput x,
y,
z in InnerVertices (GFA2AdderStr x,y,z) )
theorem
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2c ] holds
(
x in InputVertices (GFA2AdderStr x,y,z) &
y in InputVertices (GFA2AdderStr x,y,z) &
z in InputVertices (GFA2AdderStr x,y,z) )
theorem
canceled;
theorem
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2c ] holds
for
s being
State of
(GFA2AdderCirc x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . z holds
(
(Following s) . [<*x,y*>,xor2c ] = a1 'xor' ('not' a2) &
(Following s) . x = a1 &
(Following s) . y = a2 &
(Following s) . z = a3 )
theorem
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2c ] holds
for
s being
State of
(GFA2AdderCirc x,y,z) for
a1a2,
a1,
a2,
a3 being
Element of
BOOLEAN st
a1a2 = s . [<*x,y*>,xor2c ] &
a1 = s . x &
a2 = s . y &
a3 = s . z holds
(Following s) . (GFA2AdderOutput x,y,z) = a1a2 'xor' ('not' a3)
theorem Th110:
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2c ] holds
for
s being
State of
(GFA2AdderCirc x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . z holds
(
(Following s,2) . (GFA2AdderOutput x,y,z) = (a1 'xor' ('not' a2)) 'xor' ('not' a3) &
(Following s,2) . [<*x,y*>,xor2c ] = a1 'xor' ('not' a2) &
(Following s,2) . x = a1 &
(Following s,2) . y = a2 &
(Following s,2) . z = a3 )
theorem Th111:
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2c ] holds
for
s being
State of
(GFA2AdderCirc x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . z holds
(Following s,2) . (GFA2AdderOutput x,y,z) = (('not' a1) 'xor' a2) 'xor' ('not' a3)
definition
let x,
y,
z be
set ;
func BitGFA2Str x,
y,
z -> non
empty non
void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals
(GFA2AdderStr x,y,z) +* (GFA2CarryStr x,y,z);
coherence
(GFA2AdderStr x,y,z) +* (GFA2CarryStr x,y,z) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
;
end;
:: deftheorem defines BitGFA2Str GFACIRC1:def 37 :
definition
let x,
y,
z be
set ;
func BitGFA2Circ x,
y,
z -> strict gate`2=den Boolean Circuit of
BitGFA2Str x,
y,
z equals
(GFA2AdderCirc x,y,z) +* (GFA2CarryCirc x,y,z);
coherence
(GFA2AdderCirc x,y,z) +* (GFA2CarryCirc x,y,z) is strict gate`2=den Boolean Circuit of BitGFA2Str x,y,z
;
end;
:: deftheorem defines BitGFA2Circ GFACIRC1:def 38 :
theorem
canceled;
theorem Th113:
for
x,
y,
z being
set holds
InnerVertices (BitGFA2Str x,y,z) = (({[<*x,y*>,xor2c ]} \/ {(GFA2AdderOutput x,y,z)}) \/ {[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]}) \/ {(GFA2CarryOutput x,y,z)}
theorem
theorem Th115:
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2c ] &
x <> [<*y,z*>,and2c ] &
y <> [<*z,x*>,and2b ] &
z <> [<*x,y*>,and2a ] holds
InputVertices (BitGFA2Str x,y,z) = {x,y,z}
theorem Th116:
theorem
theorem
for
x,
y,
z being
set holds
(
x in the
carrier of
(BitGFA2Str x,y,z) &
y in the
carrier of
(BitGFA2Str x,y,z) &
z in the
carrier of
(BitGFA2Str x,y,z) &
[<*x,y*>,xor2c ] in the
carrier of
(BitGFA2Str x,y,z) &
[<*[<*x,y*>,xor2c ],z*>,xor2c ] in the
carrier of
(BitGFA2Str x,y,z) &
[<*x,y*>,and2a ] in the
carrier of
(BitGFA2Str x,y,z) &
[<*y,z*>,and2c ] in the
carrier of
(BitGFA2Str x,y,z) &
[<*z,x*>,and2b ] in the
carrier of
(BitGFA2Str x,y,z) &
[<*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 ] in the
carrier of
(BitGFA2Str x,y,z) )
theorem Th119:
for
x,
y,
z being
set holds
(
[<*x,y*>,xor2c ] in InnerVertices (BitGFA2Str x,y,z) &
GFA2AdderOutput x,
y,
z in InnerVertices (BitGFA2Str x,y,z) &
[<*x,y*>,and2a ] in InnerVertices (BitGFA2Str x,y,z) &
[<*y,z*>,and2c ] in InnerVertices (BitGFA2Str x,y,z) &
[<*z,x*>,and2b ] in InnerVertices (BitGFA2Str x,y,z) &
GFA2CarryOutput x,
y,
z in InnerVertices (BitGFA2Str x,y,z) )
theorem
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2c ] &
x <> [<*y,z*>,and2c ] &
y <> [<*z,x*>,and2b ] &
z <> [<*x,y*>,and2a ] holds
(
x in InputVertices (BitGFA2Str x,y,z) &
y in InputVertices (BitGFA2Str x,y,z) &
z in InputVertices (BitGFA2Str x,y,z) )
definition
let x,
y,
z be
set ;
func BitGFA2CarryOutput x,
y,
z -> Element of
InnerVertices (BitGFA2Str x,y,z) equals
[<*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 ];
coherence
[<*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 ] is Element of InnerVertices (BitGFA2Str x,y,z)
end;
:: deftheorem defines BitGFA2CarryOutput GFACIRC1:def 39 :
for
x,
y,
z being
set holds
BitGFA2CarryOutput x,
y,
z = [<*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 ];
definition
let x,
y,
z be
set ;
func BitGFA2AdderOutput x,
y,
z -> Element of
InnerVertices (BitGFA2Str x,y,z) equals
2GatesCircOutput x,
y,
z,
xor2c ;
coherence
2GatesCircOutput x,y,z,xor2c is Element of InnerVertices (BitGFA2Str x,y,z)
end;
:: deftheorem defines BitGFA2AdderOutput GFACIRC1:def 40 :
theorem
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2c ] &
x <> [<*y,z*>,and2c ] &
y <> [<*z,x*>,and2b ] &
z <> [<*x,y*>,and2a ] holds
for
s being
State of
(BitGFA2Circ x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . z holds
(
(Following s,2) . (GFA2AdderOutput x,y,z) = (('not' a1) 'xor' a2) 'xor' ('not' a3) &
(Following s,2) . (GFA2CarryOutput x,y,z) = 'not' (((('not' a1) '&' a2) 'or' (a2 '&' ('not' a3))) 'or' (('not' a3) '&' ('not' a1))) )
theorem
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2c ] &
x <> [<*y,z*>,and2c ] &
y <> [<*z,x*>,and2b ] &
z <> [<*x,y*>,and2a ] holds
for
s being
State of
(BitGFA2Circ x,y,z) holds
Following s,2 is
stable
begin
definition
let x,
y,
z be
set ;
func GFA3CarryIStr x,
y,
z -> non
empty non
void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals
((1GateCircStr <*x,y*>,and2b ) +* (1GateCircStr <*y,z*>,and2b )) +* (1GateCircStr <*z,x*>,and2b );
coherence
((1GateCircStr <*x,y*>,and2b ) +* (1GateCircStr <*y,z*>,and2b )) +* (1GateCircStr <*z,x*>,and2b ) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
;
end;
:: deftheorem defines GFA3CarryIStr GFACIRC1:def 41 :
for
x,
y,
z being
set holds
GFA3CarryIStr x,
y,
z = ((1GateCircStr <*x,y*>,and2b ) +* (1GateCircStr <*y,z*>,and2b )) +* (1GateCircStr <*z,x*>,and2b );
definition
let x,
y,
z be
set ;
func GFA3CarryICirc x,
y,
z -> strict gate`2=den Boolean Circuit of
GFA3CarryIStr x,
y,
z equals
((1GateCircuit x,y,and2b ) +* (1GateCircuit y,z,and2b )) +* (1GateCircuit z,x,and2b );
coherence
((1GateCircuit x,y,and2b ) +* (1GateCircuit y,z,and2b )) +* (1GateCircuit z,x,and2b ) is strict gate`2=den Boolean Circuit of GFA3CarryIStr x,y,z
;
end;
:: deftheorem defines GFA3CarryICirc GFACIRC1:def 42 :
for
x,
y,
z being
set holds
GFA3CarryICirc x,
y,
z = ((1GateCircuit x,y,and2b ) +* (1GateCircuit y,z,and2b )) +* (1GateCircuit z,x,and2b );
definition
let x,
y,
z be
set ;
func GFA3CarryStr x,
y,
z -> non
empty non
void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals
(GFA3CarryIStr x,y,z) +* (1GateCircStr <*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 );
coherence
(GFA3CarryIStr x,y,z) +* (1GateCircStr <*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
;
end;
:: deftheorem defines GFA3CarryStr GFACIRC1:def 43 :
for
x,
y,
z being
set holds
GFA3CarryStr x,
y,
z = (GFA3CarryIStr x,y,z) +* (1GateCircStr <*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 );
definition
let x,
y,
z be
set ;
func GFA3CarryCirc x,
y,
z -> strict gate`2=den Boolean Circuit of
GFA3CarryStr x,
y,
z equals
(GFA3CarryICirc x,y,z) +* (1GateCircuit [<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ],nor3 );
coherence
(GFA3CarryICirc x,y,z) +* (1GateCircuit [<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ],nor3 ) is strict gate`2=den Boolean Circuit of GFA3CarryStr x,y,z
;
end;
:: deftheorem defines GFA3CarryCirc GFACIRC1:def 44 :
for
x,
y,
z being
set holds
GFA3CarryCirc x,
y,
z = (GFA3CarryICirc x,y,z) +* (1GateCircuit [<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ],nor3 );
definition
let x,
y,
z be
set ;
func GFA3CarryOutput x,
y,
z -> Element of
InnerVertices (GFA3CarryStr x,y,z) equals
[<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ];
coherence
[<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ] is Element of InnerVertices (GFA3CarryStr x,y,z)
end;
:: deftheorem defines GFA3CarryOutput GFACIRC1:def 45 :
for
x,
y,
z being
set holds
GFA3CarryOutput x,
y,
z = [<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ];
theorem Th123:
for
x,
y,
z being
set holds
InnerVertices (GFA3CarryIStr x,y,z) = {[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]}
theorem Th124:
for
x,
y,
z being
set holds
InnerVertices (GFA3CarryStr x,y,z) = {[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]} \/ {(GFA3CarryOutput x,y,z)}
theorem Th125:
theorem Th126:
for
x,
y,
z being
set st
x <> [<*y,z*>,and2b ] &
y <> [<*z,x*>,and2b ] &
z <> [<*x,y*>,and2b ] holds
InputVertices (GFA3CarryIStr x,y,z) = {x,y,z}
theorem Th127:
for
x,
y,
z being
set st
x <> [<*y,z*>,and2b ] &
y <> [<*z,x*>,and2b ] &
z <> [<*x,y*>,and2b ] holds
InputVertices (GFA3CarryStr x,y,z) = {x,y,z}
theorem
theorem Th129:
for
x,
y,
z being
set holds
(
x in the
carrier of
(GFA3CarryStr x,y,z) &
y in the
carrier of
(GFA3CarryStr x,y,z) &
z in the
carrier of
(GFA3CarryStr x,y,z) &
[<*x,y*>,and2b ] in the
carrier of
(GFA3CarryStr x,y,z) &
[<*y,z*>,and2b ] in the
carrier of
(GFA3CarryStr x,y,z) &
[<*z,x*>,and2b ] in the
carrier of
(GFA3CarryStr x,y,z) &
[<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ] in the
carrier of
(GFA3CarryStr x,y,z) )
theorem Th130:
for
x,
y,
z being
set holds
(
[<*x,y*>,and2b ] in InnerVertices (GFA3CarryStr x,y,z) &
[<*y,z*>,and2b ] in InnerVertices (GFA3CarryStr x,y,z) &
[<*z,x*>,and2b ] in InnerVertices (GFA3CarryStr x,y,z) &
GFA3CarryOutput x,
y,
z in InnerVertices (GFA3CarryStr x,y,z) )
theorem Th131:
for
x,
y,
z being
set st
x <> [<*y,z*>,and2b ] &
y <> [<*z,x*>,and2b ] &
z <> [<*x,y*>,and2b ] holds
(
x in InputVertices (GFA3CarryStr x,y,z) &
y in InputVertices (GFA3CarryStr x,y,z) &
z in InputVertices (GFA3CarryStr x,y,z) )
theorem Th132:
theorem Th133:
for
x,
y,
z being
set for
s being
State of
(GFA3CarryCirc x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . z holds
(
(Following s) . [<*x,y*>,and2b ] = ('not' a1) '&' ('not' a2) &
(Following s) . [<*y,z*>,and2b ] = ('not' a2) '&' ('not' a3) &
(Following s) . [<*z,x*>,and2b ] = ('not' a3) '&' ('not' a1) )
theorem Th134:
for
x,
y,
z being
set for
s being
State of
(GFA3CarryCirc x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . [<*x,y*>,and2b ] &
a2 = s . [<*y,z*>,and2b ] &
a3 = s . [<*z,x*>,and2b ] holds
(Following s) . (GFA3CarryOutput x,y,z) = 'not' ((a1 'or' a2) 'or' a3)
theorem Th135:
for
x,
y,
z being
set st
x <> [<*y,z*>,and2b ] &
y <> [<*z,x*>,and2b ] &
z <> [<*x,y*>,and2b ] holds
for
s being
State of
(GFA3CarryCirc x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . z holds
(
(Following s,2) . (GFA3CarryOutput x,y,z) = 'not' (((('not' a1) '&' ('not' a2)) 'or' (('not' a2) '&' ('not' a3))) 'or' (('not' a3) '&' ('not' a1))) &
(Following s,2) . [<*x,y*>,and2b ] = ('not' a1) '&' ('not' a2) &
(Following s,2) . [<*y,z*>,and2b ] = ('not' a2) '&' ('not' a3) &
(Following s,2) . [<*z,x*>,and2b ] = ('not' a3) '&' ('not' a1) )
theorem Th136:
for
x,
y,
z being
set st
x <> [<*y,z*>,and2b ] &
y <> [<*z,x*>,and2b ] &
z <> [<*x,y*>,and2b ] holds
for
s being
State of
(GFA3CarryCirc x,y,z) holds
Following s,2 is
stable
definition
let x,
y,
z be
set ;
func GFA3AdderStr x,
y,
z -> non
empty non
void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals
2GatesCircStr x,
y,
z,
xor2 ;
coherence
2GatesCircStr x,y,z,xor2 is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
;
end;
:: deftheorem defines GFA3AdderStr GFACIRC1:def 46 :
definition
let x,
y,
z be
set ;
func GFA3AdderCirc x,
y,
z -> strict gate`2=den Boolean Circuit of
GFA3AdderStr x,
y,
z equals
2GatesCircuit x,
y,
z,
xor2 ;
coherence
2GatesCircuit x,y,z,xor2 is strict gate`2=den Boolean Circuit of GFA3AdderStr x,y,z
;
end;
:: deftheorem defines GFA3AdderCirc GFACIRC1:def 47 :
definition
let x,
y,
z be
set ;
func GFA3AdderOutput x,
y,
z -> Element of
InnerVertices (GFA3AdderStr x,y,z) equals
2GatesCircOutput x,
y,
z,
xor2 ;
coherence
2GatesCircOutput x,y,z,xor2 is Element of InnerVertices (GFA3AdderStr x,y,z)
;
end;
:: deftheorem defines GFA3AdderOutput GFACIRC1:def 48 :
theorem Th137:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
for
x,
y,
z being
set holds
(
x in the
carrier of
(GFA3AdderStr x,y,z) &
y in the
carrier of
(GFA3AdderStr x,y,z) &
z in the
carrier of
(GFA3AdderStr x,y,z) &
[<*x,y*>,xor2 ] in the
carrier of
(GFA3AdderStr x,y,z) &
[<*[<*x,y*>,xor2 ],z*>,xor2 ] in the
carrier of
(GFA3AdderStr x,y,z) )
by FACIRC_1:60, FACIRC_1:61;
theorem
for
x,
y,
z being
set holds
(
[<*x,y*>,xor2 ] in InnerVertices (GFA3AdderStr x,y,z) &
GFA3AdderOutput x,
y,
z in InnerVertices (GFA3AdderStr x,y,z) )
theorem
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2 ] holds
(
x in InputVertices (GFA3AdderStr x,y,z) &
y in InputVertices (GFA3AdderStr x,y,z) &
z in InputVertices (GFA3AdderStr x,y,z) )
theorem
canceled;
theorem
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2 ] holds
for
s being
State of
(GFA3AdderCirc x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . z holds
(
(Following s) . [<*x,y*>,xor2 ] = a1 'xor' a2 &
(Following s) . x = a1 &
(Following s) . y = a2 &
(Following s) . z = a3 )
theorem
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2 ] holds
for
s being
State of
(GFA3AdderCirc x,y,z) for
a1a2,
a1,
a2,
a3 being
Element of
BOOLEAN st
a1a2 = s . [<*x,y*>,xor2 ] &
a1 = s . x &
a2 = s . y &
a3 = s . z holds
(Following s) . (GFA3AdderOutput x,y,z) = a1a2 'xor' a3
theorem Th147:
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2 ] holds
for
s being
State of
(GFA3AdderCirc x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . z holds
(
(Following s,2) . (GFA3AdderOutput x,y,z) = (a1 'xor' a2) 'xor' a3 &
(Following s,2) . [<*x,y*>,xor2 ] = a1 'xor' a2 &
(Following s,2) . x = a1 &
(Following s,2) . y = a2 &
(Following s,2) . z = a3 )
theorem Th148:
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2 ] holds
for
s being
State of
(GFA3AdderCirc x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . z holds
(Following s,2) . (GFA3AdderOutput x,y,z) = 'not' ((('not' a1) 'xor' ('not' a2)) 'xor' ('not' a3))
definition
let x,
y,
z be
set ;
func BitGFA3Str x,
y,
z -> non
empty non
void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals
(GFA3AdderStr x,y,z) +* (GFA3CarryStr x,y,z);
coherence
(GFA3AdderStr x,y,z) +* (GFA3CarryStr x,y,z) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
;
end;
:: deftheorem defines BitGFA3Str GFACIRC1:def 49 :
definition
let x,
y,
z be
set ;
func BitGFA3Circ x,
y,
z -> strict gate`2=den Boolean Circuit of
BitGFA3Str x,
y,
z equals
(GFA3AdderCirc x,y,z) +* (GFA3CarryCirc x,y,z);
coherence
(GFA3AdderCirc x,y,z) +* (GFA3CarryCirc x,y,z) is strict gate`2=den Boolean Circuit of BitGFA3Str x,y,z
;
end;
:: deftheorem defines BitGFA3Circ GFACIRC1:def 50 :
theorem
canceled;
theorem Th150:
for
x,
y,
z being
set holds
InnerVertices (BitGFA3Str x,y,z) = (({[<*x,y*>,xor2 ]} \/ {(GFA3AdderOutput x,y,z)}) \/ {[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]}) \/ {(GFA3CarryOutput x,y,z)}
theorem
theorem Th152:
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2 ] &
x <> [<*y,z*>,and2b ] &
y <> [<*z,x*>,and2b ] &
z <> [<*x,y*>,and2b ] holds
InputVertices (BitGFA3Str x,y,z) = {x,y,z}
theorem Th153:
theorem
theorem
for
x,
y,
z being
set holds
(
x in the
carrier of
(BitGFA3Str x,y,z) &
y in the
carrier of
(BitGFA3Str x,y,z) &
z in the
carrier of
(BitGFA3Str x,y,z) &
[<*x,y*>,xor2 ] in the
carrier of
(BitGFA3Str x,y,z) &
[<*[<*x,y*>,xor2 ],z*>,xor2 ] in the
carrier of
(BitGFA3Str x,y,z) &
[<*x,y*>,and2b ] in the
carrier of
(BitGFA3Str x,y,z) &
[<*y,z*>,and2b ] in the
carrier of
(BitGFA3Str x,y,z) &
[<*z,x*>,and2b ] in the
carrier of
(BitGFA3Str x,y,z) &
[<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ] in the
carrier of
(BitGFA3Str x,y,z) )
theorem Th156:
for
x,
y,
z being
set holds
(
[<*x,y*>,xor2 ] in InnerVertices (BitGFA3Str x,y,z) &
GFA3AdderOutput x,
y,
z in InnerVertices (BitGFA3Str x,y,z) &
[<*x,y*>,and2b ] in InnerVertices (BitGFA3Str x,y,z) &
[<*y,z*>,and2b ] in InnerVertices (BitGFA3Str x,y,z) &
[<*z,x*>,and2b ] in InnerVertices (BitGFA3Str x,y,z) &
GFA3CarryOutput x,
y,
z in InnerVertices (BitGFA3Str x,y,z) )
theorem
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2 ] &
x <> [<*y,z*>,and2b ] &
y <> [<*z,x*>,and2b ] &
z <> [<*x,y*>,and2b ] holds
(
x in InputVertices (BitGFA3Str x,y,z) &
y in InputVertices (BitGFA3Str x,y,z) &
z in InputVertices (BitGFA3Str x,y,z) )
definition
let x,
y,
z be
set ;
func BitGFA3CarryOutput x,
y,
z -> Element of
InnerVertices (BitGFA3Str x,y,z) equals
[<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ];
coherence
[<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ] is Element of InnerVertices (BitGFA3Str x,y,z)
end;
:: deftheorem defines BitGFA3CarryOutput GFACIRC1:def 51 :
for
x,
y,
z being
set holds
BitGFA3CarryOutput x,
y,
z = [<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ];
definition
let x,
y,
z be
set ;
func BitGFA3AdderOutput x,
y,
z -> Element of
InnerVertices (BitGFA3Str x,y,z) equals
2GatesCircOutput x,
y,
z,
xor2 ;
coherence
2GatesCircOutput x,y,z,xor2 is Element of InnerVertices (BitGFA3Str x,y,z)
end;
:: deftheorem defines BitGFA3AdderOutput GFACIRC1:def 52 :
theorem
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2 ] &
x <> [<*y,z*>,and2b ] &
y <> [<*z,x*>,and2b ] &
z <> [<*x,y*>,and2b ] holds
for
s being
State of
(BitGFA3Circ x,y,z) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . z holds
(
(Following s,2) . (GFA3AdderOutput x,y,z) = 'not' ((('not' a1) 'xor' ('not' a2)) 'xor' ('not' a3)) &
(Following s,2) . (GFA3CarryOutput x,y,z) = 'not' (((('not' a1) '&' ('not' a2)) 'or' (('not' a2) '&' ('not' a3))) 'or' (('not' a3) '&' ('not' a1))) )
theorem
for
x,
y,
z being
set st
z <> [<*x,y*>,xor2 ] &
x <> [<*y,z*>,and2b ] &
y <> [<*z,x*>,and2b ] &
z <> [<*x,y*>,and2b ] holds
for
s being
State of
(BitGFA3Circ x,y,z) holds
Following s,2 is
stable