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

definition
let n be Nat;
let x, y be FinSequence;
A1: ( 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) is unsplit & 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) is gate`1=arity & 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) is gate`2isBoolean & not 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) is void & not 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) is empty & 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) is strict ) ;
func n -BitSubtracterStr x,y -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign means :Def1: :: FSCIRC_2:def 1
ex f, g being ManySortedSet of NAT st
( it = f . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & g . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = g . n holds
( f . (n + 1) = S +* (BitSubtracterWithBorrowStr (x . (n + 1)),(y . (n + 1)),z) & g . (n + 1) = BorrowOutput (x . (n + 1)),(y . (n + 1)),z ) ) );
uniqueness
for b1, b2 being non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st ex f, g being ManySortedSet of NAT st
( b1 = f . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & g . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = g . n holds
( f . (n + 1) = S +* (BitSubtracterWithBorrowStr (x . (n + 1)),(y . (n + 1)),z) & g . (n + 1) = BorrowOutput (x . (n + 1)),(y . (n + 1)),z ) ) ) & ex f, g being ManySortedSet of NAT st
( b2 = f . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & g . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = g . n holds
( f . (n + 1) = S +* (BitSubtracterWithBorrowStr (x . (n + 1)),(y . (n + 1)),z) & g . (n + 1) = BorrowOutput (x . (n + 1)),(y . (n + 1)),z ) ) ) holds
b1 = b2
proof end;
existence
ex b1 being non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign ex f, g being ManySortedSet of NAT st
( b1 = f . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & g . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = g . n holds
( f . (n + 1) = S +* (BitSubtracterWithBorrowStr (x . (n + 1)),(y . (n + 1)),z) & g . (n + 1) = BorrowOutput (x . (n + 1)),(y . (n + 1)),z ) ) )
proof end;
end;

:: deftheorem Def1 defines -BitSubtracterStr FSCIRC_2:def 1 :
for n being Nat
for x, y being FinSequence
for b4 being non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign holds
( b4 = n -BitSubtracterStr x,y iff ex f, g being ManySortedSet of NAT st
( b4 = f . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & g . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = g . n holds
( f . (n + 1) = S +* (BitSubtracterWithBorrowStr (x . (n + 1)),(y . (n + 1)),z) & g . (n + 1) = BorrowOutput (x . (n + 1)),(y . (n + 1)),z ) ) ) );

definition
let n be Nat;
let x, y be FinSequence;
func n -BitSubtracterCirc x,y -> strict gate`2=den Boolean Circuit of n -BitSubtracterStr x,y means :Def2: :: FSCIRC_2:def 2
ex f, g, h being ManySortedSet of NAT st
( n -BitSubtracterStr x,y = f . n & it = g . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & g . 0 = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = S +* (BitSubtracterWithBorrowStr (x . (n + 1)),(y . (n + 1)),z) & g . (n + 1) = A +* (BitSubtracterWithBorrowCirc (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = BorrowOutput (x . (n + 1)),(y . (n + 1)),z ) ) );
uniqueness
for b1, b2 being strict gate`2=den Boolean Circuit of n -BitSubtracterStr x,y st ex f, g, h being ManySortedSet of NAT st
( n -BitSubtracterStr x,y = f . n & b1 = g . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & g . 0 = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = S +* (BitSubtracterWithBorrowStr (x . (n + 1)),(y . (n + 1)),z) & g . (n + 1) = A +* (BitSubtracterWithBorrowCirc (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = BorrowOutput (x . (n + 1)),(y . (n + 1)),z ) ) ) & ex f, g, h being ManySortedSet of NAT st
( n -BitSubtracterStr x,y = f . n & b2 = g . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & g . 0 = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = S +* (BitSubtracterWithBorrowStr (x . (n + 1)),(y . (n + 1)),z) & g . (n + 1) = A +* (BitSubtracterWithBorrowCirc (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = BorrowOutput (x . (n + 1)),(y . (n + 1)),z ) ) ) holds
b1 = b2
proof end;
existence
ex b1 being strict gate`2=den Boolean Circuit of n -BitSubtracterStr x,y ex f, g, h being ManySortedSet of NAT st
( n -BitSubtracterStr x,y = f . n & b1 = g . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & g . 0 = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = S +* (BitSubtracterWithBorrowStr (x . (n + 1)),(y . (n + 1)),z) & g . (n + 1) = A +* (BitSubtracterWithBorrowCirc (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = BorrowOutput (x . (n + 1)),(y . (n + 1)),z ) ) )
proof end;
end;

:: deftheorem Def2 defines -BitSubtracterCirc FSCIRC_2:def 2 :
for n being Nat
for x, y being FinSequence
for b4 being strict gate`2=den Boolean Circuit of n -BitSubtracterStr x,y holds
( b4 = n -BitSubtracterCirc x,y iff ex f, g, h being ManySortedSet of NAT st
( n -BitSubtracterStr x,y = f . n & b4 = g . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & g . 0 = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = S +* (BitSubtracterWithBorrowStr (x . (n + 1)),(y . (n + 1)),z) & g . (n + 1) = A +* (BitSubtracterWithBorrowCirc (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = BorrowOutput (x . (n + 1)),(y . (n + 1)),z ) ) ) );

definition
let n be Nat;
let x, y be FinSequence;
set c = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )];
func n -BitBorrowOutput x,y -> Element of InnerVertices (n -BitSubtracterStr x,y) means :Def3: :: FSCIRC_2:def 3
ex h being ManySortedSet of NAT st
( it = h . n & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat holds h . (n + 1) = BorrowOutput (x . (n + 1)),(y . (n + 1)),(h . n) ) );
uniqueness
for b1, b2 being Element of InnerVertices (n -BitSubtracterStr x,y) st ex h being ManySortedSet of NAT st
( b1 = h . n & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat holds h . (n + 1) = BorrowOutput (x . (n + 1)),(y . (n + 1)),(h . n) ) ) & ex h being ManySortedSet of NAT st
( b2 = h . n & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat holds h . (n + 1) = BorrowOutput (x . (n + 1)),(y . (n + 1)),(h . n) ) ) holds
b1 = b2
proof end;
existence
ex b1 being Element of InnerVertices (n -BitSubtracterStr x,y) ex h being ManySortedSet of NAT st
( b1 = h . n & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat holds h . (n + 1) = BorrowOutput (x . (n + 1)),(y . (n + 1)),(h . n) ) )
proof end;
end;

:: deftheorem Def3 defines -BitBorrowOutput FSCIRC_2:def 3 :
for n being Nat
for x, y being FinSequence
for b4 being Element of InnerVertices (n -BitSubtracterStr x,y) holds
( b4 = n -BitBorrowOutput x,y iff ex h being ManySortedSet of NAT st
( b4 = h . n & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat holds h . (n + 1) = BorrowOutput (x . (n + 1)),(y . (n + 1)),(h . n) ) ) );

theorem Th1: :: FSCIRC_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being FinSequence
for f, g, h being ManySortedSet of NAT st f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & g . 0 = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = S +* (BitSubtracterWithBorrowStr (x . (n + 1)),(y . (n + 1)),z) & g . (n + 1) = A +* (BitSubtracterWithBorrowCirc (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = BorrowOutput (x . (n + 1)),(y . (n + 1)),z ) ) holds
for n being Nat holds
( n -BitSubtracterStr x,y = f . n & n -BitSubtracterCirc x,y = g . n & n -BitBorrowOutput x,y = h . n )
proof end;

theorem Th2: :: FSCIRC_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being FinSequence holds
( 0 -BitSubtracterStr a,b = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & 0 -BitSubtracterCirc a,b = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & 0 -BitBorrowOutput a,b = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] )
proof end;

theorem Th3: :: FSCIRC_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being FinSequence
for c being set st c = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] holds
( 1 -BitSubtracterStr a,b = (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE )) +* (BitSubtracterWithBorrowStr (a . 1),(b . 1),c) & 1 -BitSubtracterCirc a,b = (1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> TRUE )) +* (BitSubtracterWithBorrowCirc (a . 1),(b . 1),c) & 1 -BitBorrowOutput a,b = BorrowOutput (a . 1),(b . 1),c )
proof end;

theorem :: FSCIRC_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being set st c = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] holds
( 1 -BitSubtracterStr <*a*>,<*b*> = (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE )) +* (BitSubtracterWithBorrowStr a,b,c) & 1 -BitSubtracterCirc <*a*>,<*b*> = (1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> TRUE )) +* (BitSubtracterWithBorrowCirc a,b,c) & 1 -BitBorrowOutput <*a*>,<*b*> = BorrowOutput a,b,c )
proof end;

theorem Th5: :: FSCIRC_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for p, q being FinSeqLen of n
for p1, p2, q1, q2 being FinSequence holds
( n -BitSubtracterStr (p ^ p1),(q ^ q1) = n -BitSubtracterStr (p ^ p2),(q ^ q2) & n -BitSubtracterCirc (p ^ p1),(q ^ q1) = n -BitSubtracterCirc (p ^ p2),(q ^ q2) & n -BitBorrowOutput (p ^ p1),(q ^ q1) = n -BitBorrowOutput (p ^ p2),(q ^ q2) )
proof end;

theorem :: FSCIRC_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for x, y being FinSeqLen of n
for a, b being set holds
( (n + 1) -BitSubtracterStr (x ^ <*a*>),(y ^ <*b*>) = (n -BitSubtracterStr x,y) +* (BitSubtracterWithBorrowStr a,b,(n -BitBorrowOutput x,y)) & (n + 1) -BitSubtracterCirc (x ^ <*a*>),(y ^ <*b*>) = (n -BitSubtracterCirc x,y) +* (BitSubtracterWithBorrowCirc a,b,(n -BitBorrowOutput x,y)) & (n + 1) -BitBorrowOutput (x ^ <*a*>),(y ^ <*b*>) = BorrowOutput a,b,(n -BitBorrowOutput x,y) )
proof end;

theorem Th7: :: FSCIRC_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for x, y being FinSequence holds
( (n + 1) -BitSubtracterStr x,y = (n -BitSubtracterStr x,y) +* (BitSubtracterWithBorrowStr (x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput x,y)) & (n + 1) -BitSubtracterCirc x,y = (n -BitSubtracterCirc x,y) +* (BitSubtracterWithBorrowCirc (x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput x,y)) & (n + 1) -BitBorrowOutput x,y = BorrowOutput (x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput x,y) )
proof end;

theorem Th8: :: FSCIRC_2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat st n <= m holds
for x, y being FinSequence holds InnerVertices (n -BitSubtracterStr x,y) c= InnerVertices (m -BitSubtracterStr x,y)
proof end;

theorem :: FSCIRC_2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for x, y being FinSequence holds InnerVertices ((n + 1) -BitSubtracterStr x,y) = (InnerVertices (n -BitSubtracterStr x,y)) \/ (InnerVertices (BitSubtracterWithBorrowStr (x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput x,y)))
proof end;

definition
let k, n be Nat;
assume A1: ( k >= 1 & k <= n ) ;
let x, y be FinSequence;
func k,n -BitSubtracterOutput x,y -> Element of InnerVertices (n -BitSubtracterStr x,y) means :Def4: :: FSCIRC_2:def 4
ex i being Nat st
( k = i + 1 & it = BitSubtracterOutput (x . k),(y . k),(i -BitBorrowOutput x,y) );
uniqueness
for b1, b2 being Element of InnerVertices (n -BitSubtracterStr x,y) st ex i being Nat st
( k = i + 1 & b1 = BitSubtracterOutput (x . k),(y . k),(i -BitBorrowOutput x,y) ) & ex i being Nat st
( k = i + 1 & b2 = BitSubtracterOutput (x . k),(y . k),(i -BitBorrowOutput x,y) ) holds
b1 = b2
;
existence
ex b1 being Element of InnerVertices (n -BitSubtracterStr x,y) ex i being Nat st
( k = i + 1 & b1 = BitSubtracterOutput (x . k),(y . k),(i -BitBorrowOutput x,y) )
proof end;
end;

:: deftheorem Def4 defines -BitSubtracterOutput FSCIRC_2:def 4 :
for k, n being Nat st k >= 1 & k <= n holds
for x, y being FinSequence
for b5 being Element of InnerVertices (n -BitSubtracterStr x,y) holds
( b5 = k,n -BitSubtracterOutput x,y iff ex i being Nat st
( k = i + 1 & b5 = BitSubtracterOutput (x . k),(y . k),(i -BitBorrowOutput x,y) ) );

theorem :: FSCIRC_2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k being Nat st k < n holds
for x, y being FinSequence holds (k + 1),n -BitSubtracterOutput x,y = BitSubtracterOutput (x . (k + 1)),(y . (k + 1)),(k -BitBorrowOutput x,y)
proof end;

theorem :: FSCIRC_2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for x, y being FinSequence holds InnerVertices (n -BitSubtracterStr x,y) is Relation
proof end;

theorem Th12: :: FSCIRC_2: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 set holds InnerVertices (BorrowIStr x,y,c) = {[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]}
proof end;

theorem Th13: :: FSCIRC_2: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 set st x <> [<*y,c*>,and2 ] & y <> [<*x,c*>,and2a ] & c <> [<*x,y*>,and2a ] holds
InputVertices (BorrowIStr x,y,c) = {x,y,c}
proof end;

theorem Th14: :: FSCIRC_2: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 set holds InnerVertices (BorrowStr x,y,c) = {[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]} \/ {(BorrowOutput x,y,c)}
proof end;

theorem Th15: :: FSCIRC_2: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 set st x <> [<*y,c*>,and2 ] & y <> [<*x,c*>,and2a ] & c <> [<*x,y*>,and2a ] holds
InputVertices (BorrowStr x,y,c) = {x,y,c}
proof end;

theorem Th16: :: FSCIRC_2: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 set st x <> [<*y,c*>,and2 ] & y <> [<*x,c*>,and2a ] & c <> [<*x,y*>,and2a ] & c <> [<*x,y*>,'xor' ] holds
InputVertices (BitSubtracterWithBorrowStr x,y,c) = {x,y,c}
proof end;

theorem Th17: :: FSCIRC_2: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 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;

registration
let n be Nat;
let x, y be FinSequence;
cluster n -BitBorrowOutput x,y -> pair ;
coherence
n -BitBorrowOutput x,y is pair
proof end;
end;

theorem Th18: :: FSCIRC_2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being FinSequence
for n being Nat holds
( ( (n -BitBorrowOutput x,y) `1 = <*> & (n -BitBorrowOutput x,y) `2 = (0 -tuples_on BOOLEAN ) --> TRUE & proj1 ((n -BitBorrowOutput x,y) `2 ) = 0 -tuples_on BOOLEAN ) or ( Card ((n -BitBorrowOutput x,y) `1 ) = 3 & (n -BitBorrowOutput x,y) `2 = or3 & proj1 ((n -BitBorrowOutput x,y) `2 ) = 3 -tuples_on BOOLEAN ) )
proof end;

theorem Th19: :: FSCIRC_2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for x, y being FinSequence
for p being set holds
( n -BitBorrowOutput x,y <> [p,and2 ] & n -BitBorrowOutput x,y <> [p,and2a ] & n -BitBorrowOutput x,y <> [p,'xor' ] )
proof end;

theorem Th20: :: FSCIRC_2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being nonpair-yielding FinSequence
for n being Nat holds
( InputVertices ((n + 1) -BitSubtracterStr f,g) = (InputVertices (n -BitSubtracterStr f,g)) \/ ((InputVertices (BitSubtracterWithBorrowStr (f . (n + 1)),(g . (n + 1)),(n -BitBorrowOutput f,g))) \ {(n -BitBorrowOutput f,g)}) & InnerVertices (n -BitSubtracterStr f,g) is Relation & not InputVertices (n -BitSubtracterStr f,g) is with_pair )
proof end;

theorem :: FSCIRC_2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for x, y being nonpair-yielding FinSeqLen of n holds InputVertices (n -BitSubtracterStr x,y) = (rng x) \/ (rng y)
proof end;

Lm1: for x, y, c being 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 Th22: :: FSCIRC_2: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
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 set st x <> [<*y,c*>,and2 ] & y <> [<*x,c*>,and2a ] & c <> [<*x,y*>,and2a ] holds
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 Th23: :: FSCIRC_2: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 set st x <> [<*y,c*>,and2 ] & y <> [<*x,c*>,and2a ] & c <> [<*x,y*>,and2a ] & c <> [<*x,y*>,'xor' ] holds
for s being State of (BorrowCirc x,y,c) holds Following s,2 is stable
proof end;

theorem :: FSCIRC_2: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 st x <> [<*y,c*>,and2 ] & y <> [<*x,c*>,and2a ] & c <> [<*x,y*>,and2a ] & c <> [<*x,y*>,'xor' ] holds
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 Th25: :: FSCIRC_2: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 set st x <> [<*y,c*>,and2 ] & y <> [<*x,c*>,and2a ] & c <> [<*x,y*>,and2a ] & c <> [<*x,y*>,'xor' ] holds
for s being State of (BitSubtracterWithBorrowCirc x,y,c) holds Following s,2 is stable
proof end;

theorem :: FSCIRC_2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for x, y being nonpair-yielding FinSeqLen of n
for s being State of (n -BitSubtracterCirc x,y) holds Following s,(1 + (2 * n)) is stable
proof end;