begin
:: deftheorem Def1 defines inv1 GFACIRC1:def 1 :
for b1 being Function of (1 -tuples_on BOOLEAN),BOOLEAN holds
( b1 = inv1 iff for x being Element of BOOLEAN holds b1 . <*x*> = 'not' x );
theorem Th1:
:: deftheorem Def2 defines buf1 GFACIRC1:def 2 :
for b1 being Function of (1 -tuples_on BOOLEAN),BOOLEAN holds
( b1 = buf1 iff for x being Element of BOOLEAN holds b1 . <*x*> = x );
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 :
for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds
( b1 = and2c iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x '&' ('not' y) );
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 :
for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds
( b1 = xor2c iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'xor' ('not' y) );
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 :
for x, y, z being set holds GFA0AdderStr (x,y,z) = 2GatesCircStr (x,y,z,xor2);
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 :
for x, y, z being set holds GFA0AdderCirc (x,y,z) = 2GatesCircuit (x,y,z,xor2);
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 :
for x, y, z being set holds GFA0AdderOutput (x,y,z) = 2GatesCircOutput (x,y,z,xor2);
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 :
for x, y, z being set holds BitGFA0Str (x,y,z) = (GFA0AdderStr (x,y,z)) +* (GFA0CarryStr (x,y,z));
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 :
for x, y, z being set holds BitGFA0Circ (x,y,z) = (GFA0AdderCirc (x,y,z)) +* (GFA0CarryCirc (x,y,z));
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 :
for x, y, z being set holds BitGFA0AdderOutput (x,y,z) = 2GatesCircOutput (x,y,z,xor2);
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 :
for x, y, z being set holds GFA1AdderStr (x,y,z) = 2GatesCircStr (x,y,z,xor2c);
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 :
for x, y, z being set holds GFA1AdderCirc (x,y,z) = 2GatesCircuit (x,y,z,xor2c);
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 :
for x, y, z being set holds GFA1AdderOutput (x,y,z) = 2GatesCircOutput (x,y,z,xor2c);
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 :
for x, y, z being set holds BitGFA1Str (x,y,z) = (GFA1AdderStr (x,y,z)) +* (GFA1CarryStr (x,y,z));
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 :
for x, y, z being set holds BitGFA1Circ (x,y,z) = (GFA1AdderCirc (x,y,z)) +* (GFA1CarryCirc (x,y,z));
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 :
for x, y, z being set holds BitGFA1AdderOutput (x,y,z) = 2GatesCircOutput (x,y,z,xor2c);
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 :
for x, y, z being set holds GFA2AdderStr (x,y,z) = 2GatesCircStr (x,y,z,xor2c);
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 :
for x, y, z being set holds GFA2AdderCirc (x,y,z) = 2GatesCircuit (x,y,z,xor2c);
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 :
for x, y, z being set holds GFA2AdderOutput (x,y,z) = 2GatesCircOutput (x,y,z,xor2c);
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 :
for x, y, z being set holds BitGFA2Str (x,y,z) = (GFA2AdderStr (x,y,z)) +* (GFA2CarryStr (x,y,z));
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 :
for x, y, z being set holds BitGFA2Circ (x,y,z) = (GFA2AdderCirc (x,y,z)) +* (GFA2CarryCirc (x,y,z));
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 :
for x, y, z being set holds BitGFA2AdderOutput (x,y,z) = 2GatesCircOutput (x,y,z,xor2c);
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 :
for x, y, z being set holds GFA3AdderStr (x,y,z) = 2GatesCircStr (x,y,z,xor2);
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 :
for x, y, z being set holds GFA3AdderCirc (x,y,z) = 2GatesCircuit (x,y,z,xor2);
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 :
for x, y, z being set holds GFA3AdderOutput (x,y,z) = 2GatesCircOutput (x,y,z,xor2);
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 :
for x, y, z being set holds BitGFA3Str (x,y,z) = (GFA3AdderStr (x,y,z)) +* (GFA3CarryStr (x,y,z));
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 :
for x, y, z being set holds BitGFA3Circ (x,y,z) = (GFA3AdderCirc (x,y,z)) +* (GFA3CarryCirc (x,y,z));
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 :
for x, y, z being set holds BitGFA3AdderOutput (x,y,z) = 2GatesCircOutput (x,y,z,xor2);
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