begin
::
deftheorem defines
BorrowIStr FSCIRC_1:def 3 :
for x, y, c being set holds BorrowIStr (x,y,c) = ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a));
definition
let x,
y,
c be
set ;
func BorrowStr (
x,
y,
c)
-> non
empty non
void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals
(BorrowIStr (x,y,c)) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3));
correctness
coherence
(BorrowIStr (x,y,c)) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;
;
end;
::
deftheorem defines
BorrowStr FSCIRC_1:def 4 :
for x, y, c being set holds BorrowStr (x,y,c) = (BorrowIStr (x,y,c)) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3));
definition
let x,
y,
c be
set ;
func BorrowICirc (
x,
y,
c)
-> strict gate`2=den Boolean Circuit of
BorrowIStr (
x,
y,
c)
equals
((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a));
coherence
((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a)) is strict gate`2=den Boolean Circuit of BorrowIStr (x,y,c)
;
end;
::
deftheorem defines
BorrowICirc FSCIRC_1:def 5 :
for x, y, c being set holds BorrowICirc (x,y,c) = ((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a));
definition
let x,
y,
c be
set ;
func BorrowOutput (
x,
y,
c)
-> Element of
InnerVertices (BorrowStr (x,y,c)) equals
[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3];
coherence
[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3] is Element of InnerVertices (BorrowStr (x,y,c))
correctness
;
end;
::
deftheorem defines
BorrowOutput FSCIRC_1:def 6 :
for x, y, c being set holds BorrowOutput (x,y,c) = [<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3];
definition
let x,
y,
c be
set ;
func BorrowCirc (
x,
y,
c)
-> strict gate`2=den Boolean Circuit of
BorrowStr (
x,
y,
c)
equals
(BorrowICirc (x,y,c)) +* (1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3));
coherence
(BorrowICirc (x,y,c)) +* (1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3)) is strict gate`2=den Boolean Circuit of BorrowStr (x,y,c)
;
end;
::
deftheorem defines
BorrowCirc FSCIRC_1:def 7 :
for x, y, c being set holds BorrowCirc (x,y,c) = (BorrowICirc (x,y,c)) +* (1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3));
theorem Th7:
for
x,
y,
c being
set holds
(
[<*x,y*>,and2a] in InnerVertices (BorrowStr (x,y,c)) &
[<*y,c*>,and2] in InnerVertices (BorrowStr (x,y,c)) &
[<*x,c*>,and2a] in InnerVertices (BorrowStr (x,y,c)) )
theorem Th9:
for
x,
y,
c being non
pair set holds
(
InputVertices (BorrowStr (x,y,c)) = {x,y,c} &
InnerVertices (BorrowStr (x,y,c)) = {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \/ {(BorrowOutput (x,y,c))} )
Lm1:
for x, y, c being non pair set
for s being State of (BorrowCirc (x,y,c))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
( (Following s) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following s) . [<*y,c*>,and2] = a2 '&' a3 & (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 )
theorem Th13:
for
x,
y,
c being non
pair set for
s being
State of
(BorrowCirc (x,y,c)) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . [<*x,y*>,and2a] &
a2 = s . [<*y,c*>,and2] &
a3 = s . [<*x,c*>,and2a] holds
(Following s) . (BorrowOutput (x,y,c)) = (a1 'or' a2) 'or' a3
Lm2:
for x, y, c being non pair set
for s being State of (BorrowCirc (x,y,c))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
( (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) & (Following (s,2)) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following (s,2)) . [<*y,c*>,and2] = a2 '&' a3 & (Following (s,2)) . [<*x,c*>,and2a] = ('not' a1) '&' a3 )
begin
theorem
for
x,
y,
c being non
pair set holds
InnerVertices (BitSubtracterWithBorrowStr (x,y,c)) = ({[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]}) \/ {(BorrowOutput (x,y,c))}
theorem
for
x,
y,
c being non
pair set for
s being
State of
(BitSubtracterWithBorrowCirc (x,y,c)) for
a1,
a2,
a3 being
Element of
BOOLEAN st
a1 = s . x &
a2 = s . y &
a3 = s . c holds
(
(Following (s,2)) . (BitSubtracterOutput (x,y,c)) = (a1 'xor' a2) 'xor' a3 &
(Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) )