:: FSCIRC_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let x, y, c be set ;
func BitSubtracterOutput x,y,c -> Element of InnerVertices (2GatesCircStr x,y,c,'xor' ) equals :: FSCIRC_1:def 1
 2GatesCircOutput x,y,c,'xor' ;
coherence
2GatesCircOutput x,y,c,'xor' is Element of InnerVertices (2GatesCircStr x,y,c,'xor' ) ;
end;

:: deftheorem defines BitSubtracterOutput FSCIRC_1:def 1 :
for x, y, c being set holds BitSubtracterOutput x,y,c = 2GatesCircOutput x,y,c,'xor' ;

definition
let x, y, c be set ;
func BitSubtracterCirc x,y,c -> strict gate`2=den Boolean Circuit of 2GatesCircStr x,y,c,'xor' equals :: FSCIRC_1:def 2
 2GatesCircuit x,y,c,'xor' ;
coherence
2GatesCircuit x,y,c,'xor' is strict gate`2=den Boolean Circuit of 2GatesCircStr x,y,c,'xor' ;
end;

:: deftheorem defines BitSubtracterCirc FSCIRC_1:def 2 :
for x, y, c being set holds BitSubtracterCirc x,y,c = 2GatesCircuit x,y,c,'xor' ;

definition
let x, y, c be set ;
func BorrowIStr x,y,c -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FSCIRC_1:def 3
((1GateCircStr <*x,y*>,and2a ) +* (1GateCircStr <*y,c*>,and2 )) +* (1GateCircStr <*x,c*>,and2a );
correctness
coherence
((1GateCircStr <*x,y*>,and2a ) +* (1GateCircStr <*y,c*>,and2 )) +* (1GateCircStr <*x,c*>,and2a ) is non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign ;
;
end;

:: 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 strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FSCIRC_1:def 4
(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 strict non void 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 :: FSCIRC_1:def 5
((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 );

theorem Th1: :: FSCIRC_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being set holds InnerVertices (BorrowStr x,y,c) is Relation
proof end;

theorem Th2: :: FSCIRC_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set holds not InputVertices (BorrowStr x,y,c) is with_pair
proof end;

theorem :: FSCIRC_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being set
for s being State of (BorrowICirc x,y,c)
for a, b being Element of BOOLEAN st a = s . x & b = s . y holds
(Following s) . [<*x,y*>,and2a ] = ('not' a) '&' b
proof end;

theorem :: FSCIRC_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being set
for s being State of (BorrowICirc x,y,c)
for a, b being Element of BOOLEAN st a = s . y & b = s . c holds
(Following s) . [<*y,c*>,and2 ] = a '&' b
proof end;

theorem :: FSCIRC_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being set
for s being State of (BorrowICirc x,y,c)
for a, b being Element of BOOLEAN st a = s . x & b = s . c holds
(Following s) . [<*x,c*>,and2a ] = ('not' a) '&' b
proof end;

definition
let x, y, c be set ;
func BorrowOutput x,y,c -> Element of InnerVertices (BorrowStr x,y,c) equals :: FSCIRC_1:def 6
[<*[<*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)
proof end;
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 :: FSCIRC_1:def 7
(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 Th6: :: FSCIRC_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being set holds
( x in the carrier of (BorrowStr x,y,c) & y in the carrier of (BorrowStr x,y,c) & c in the carrier of (BorrowStr x,y,c) )
proof end;

theorem Th7: :: FSCIRC_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem Th8: :: FSCIRC_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set holds
( x in InputVertices (BorrowStr x,y,c) & y in InputVertices (BorrowStr x,y,c) & c in InputVertices (BorrowStr x,y,c) )
proof end;

theorem Th9: :: FSCIRC_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)} )
proof end;

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 )
proof end;

theorem :: FSCIRC_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set
for s being State of (BorrowCirc x,y,c)
for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds
(Following s) . [<*x,y*>,and2a ] = ('not' a1) '&' a2
proof end;

theorem :: FSCIRC_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set
for s being State of (BorrowCirc x,y,c)
for a2, a3 being Element of BOOLEAN st a2 = s . y & a3 = s . c holds
(Following s) . [<*y,c*>,and2 ] = a2 '&' a3
proof end;

theorem :: FSCIRC_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set
for s being State of (BorrowCirc x,y,c)
for a1, a3 being Element of BOOLEAN st a1 = s . x & a3 = s . c holds
(Following s) . [<*x,c*>,and2a ] = ('not' a1) '&' a3
proof end;

theorem Th13: :: FSCIRC_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

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 )
proof end;

theorem :: FSCIRC_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set
for s being State of (BorrowCirc x,y,c)
for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds
(Following s,2) . [<*x,y*>,and2a ] = ('not' a1) '&' a2
proof end;

theorem :: FSCIRC_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set
for s being State of (BorrowCirc x,y,c)
for a2, a3 being Element of BOOLEAN st a2 = s . y & a3 = s . c holds
(Following s,2) . [<*y,c*>,and2 ] = a2 '&' a3
proof end;

theorem :: FSCIRC_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set
for s being State of (BorrowCirc x,y,c)
for a1, a3 being Element of BOOLEAN st a1 = s . x & a3 = s . c holds
(Following s,2) . [<*x,c*>,and2a ] = ('not' a1) '&' a3
proof end;

theorem :: FSCIRC_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) by Lm2;

theorem Th18: :: FSCIRC_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set
for s being State of (BorrowCirc x,y,c) holds Following s,2 is stable
proof end;

definition
let x, y, c be set ;
func BitSubtracterWithBorrowStr x,y,c -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FSCIRC_1:def 8
(2GatesCircStr x,y,c,'xor' ) +* (BorrowStr x,y,c);
coherence
(2GatesCircStr x,y,c,'xor' ) +* (BorrowStr x,y,c) is non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign ;
end;

:: deftheorem defines BitSubtracterWithBorrowStr FSCIRC_1:def 8 :
for x, y, c being set holds BitSubtracterWithBorrowStr x,y,c = (2GatesCircStr x,y,c,'xor' ) +* (BorrowStr x,y,c);

theorem Th19: :: FSCIRC_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set holds InputVertices (BitSubtracterWithBorrowStr x,y,c) = {x,y,c}
proof end;

theorem :: FSCIRC_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)}
proof end;

theorem :: FSCIRC_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being set
for S being non empty ManySortedSign st S = BitSubtracterWithBorrowStr x,y,c holds
( x in the carrier of S & y in the carrier of S & c in the carrier of S )
proof end;

definition
let x, y, c be set ;
func BitSubtracterWithBorrowCirc x,y,c -> strict gate`2=den Boolean Circuit of BitSubtracterWithBorrowStr x,y,c equals :: FSCIRC_1:def 9
(BitSubtracterCirc x,y,c) +* (BorrowCirc x,y,c);
coherence
(BitSubtracterCirc x,y,c) +* (BorrowCirc x,y,c) is strict gate`2=den Boolean Circuit of BitSubtracterWithBorrowStr x,y,c ;
end;

:: deftheorem defines BitSubtracterWithBorrowCirc FSCIRC_1:def 9 :
for x, y, c being set holds BitSubtracterWithBorrowCirc x,y,c = (BitSubtracterCirc x,y,c) +* (BorrowCirc x,y,c);

theorem :: FSCIRC_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being set holds InnerVertices (BitSubtracterWithBorrowStr x,y,c) is Relation
proof end;

theorem :: FSCIRC_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set holds not InputVertices (BitSubtracterWithBorrowStr x,y,c) is with_pair
proof end;

theorem :: FSCIRC_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being set holds
( BitSubtracterOutput x,y,c in InnerVertices (BitSubtracterWithBorrowStr x,y,c) & BorrowOutput x,y,c in InnerVertices (BitSubtracterWithBorrowStr x,y,c) ) by FACIRC_1:21;

theorem :: FSCIRC_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: FSCIRC_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set
for s being State of (BitSubtracterWithBorrowCirc x,y,c) holds Following s,2 is stable
proof end;