:: Full Subtracter Circuit. Part {II}
:: by Shin'nosuke Yamaguchi , Grzegorz Bancerek and Katsumi Wasaki
::
:: Received February 25, 2003
:: Copyright (c) 2003-2021 Association of Mizar Users


::------------------------------------------------------------
:: Definitions of n-Bit Full Subtracter Structure and Circuit
::------------------------------------------------------------
definition
let n be Nat;
let x, y be FinSequence;
deffunc H1( set , Nat) -> Element of InnerVertices (BorrowStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = BorrowOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1);
deffunc H2( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitSubtracterWithBorrowStr ((x . ($3 + 1)),(y . ($3 + 1)),$2));
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 non void strict 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 non void strict 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 non void strict 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 non void strict 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 over 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 over 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 over 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 over 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 over 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)) ) ) );

::------------------------------------------------------------
:: Properties of n-Bit Full Subtracter Structure and Circuit
::------------------------------------------------------------
theorem Th1: :: FSCIRC_2:1
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 over 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
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
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
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
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
for n being Element of 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
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;

::------------------------------------------------------------
:: Inner and Input-Vertex of n-Bit Full Subtracter Structure
::------------------------------------------------------------
theorem Th8: :: FSCIRC_2:8
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
for n being Element of 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 that
A1: k >= 1 and
A2: 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 Element of 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 Element of NAT st
( k = i + 1 & b1 = BitSubtracterOutput ((x . k),(y . k),(i -BitBorrowOutput (x,y))) ) & ex i being Element of 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 Element of 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 Element of NAT st
( k = i + 1 & b5 = BitSubtracterOutput ((x . k),(y . k),(i -BitBorrowOutput (x,y))) ) );

theorem :: FSCIRC_2:10
for n, k being Element of 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
for n being Element of NAT
for x, y being FinSequence holds InnerVertices (n -BitSubtracterStr (x,y)) is Relation
proof end;

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

::-----------------------------------------------------
:: Relation and Pair for n-Bit Full Subtracter
::-----------------------------------------------------
theorem Th20: :: FSCIRC_2:20
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 & InputVertices (n -BitSubtracterStr (f,g)) is without_pairs )
proof end;

theorem :: FSCIRC_2:21
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
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
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)) holds Following (s,2) is stable
proof end;

theorem :: FSCIRC_2:24
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
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
for n being Element of 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;