let n be Element of NAT ; :: thesis:
let f, g be nonpair-yielding FinSeqLen of n; :: thesis:
deffunc H₁( set , Nat) -> ManySortedSign = BitSubtracterWithBorrowStr ((f . ($2 + 1)),(g . ($2 + 1)),$1);
deffunc H₂( set , Nat) -> MSAlgebra over BitSubtracterWithBorrowStr ((f . ($2 + 1)),(g . ($2 + 1)),$1) = BitSubtracterWithBorrowCirc ((f . ($2 + 1)),(g . ($2 + 1)),$1);
deffunc H₃( set , Nat) -> Element of InnerVertices (BorrowStr ((f . ($2 + 1)),(g . ($2 + 1)),$1)) = BorrowOutput ((f . ($2 + 1)),(g . ($2 + 1)),$1);
set S0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE));
set A0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE));
set N = (1,2) followed_by (In (n,NAT));
A1: ((1,2) followed_by (In (n,NAT))) . 0 = 1 by FUNCT_7:122;
A2: ((1,2) followed_by (In (n,NAT))) . 1 = 2 by FUNCT_7:123;
A3: ((1,2) followed_by (In (n,NAT))) . 2 = n by FUNCT_7:124;
deffunc H₄( Element of NAT ) -> Element of NAT = ((1,2) followed_by (In (n,NAT))) . $1;
A4: for x being set
for n being Nat holds H₂(x,n) is strict gate`2=den Boolean Circuit of H₁(x,n) ;

end;

deffunc H₅( Element of NAT ) -> Element of InnerVertices ($1 -BitSubtracterStr (f,g)) = $1 -BitBorrowOutput (f,g);
consider h being ManySortedSet of NAT such that
A6: for n being Element of NAT holds h . n = H₅(n) from PBOOLE:sch 5();
A7: for n being Nat
for x being set
for A being non-empty Circuit of H₁(x,n) st x = h . n & A = H₂(x,n) holds
for s being State of A holds Following (s,H₄(1)) is stable

let n be Nat; :: thesis:
let x be set ; :: thesis:
let A be non-empty Circuit of H₁(x,n); :: thesis:
A8: n in NAT by ORDINAL1:def 12;
assume x = h . n ; :: thesis:
then A9: x = n -BitBorrowOutput (f,g) by A6, A8;
then A10: x <> [<*(f . (n + 1)),(g . (n + 1))*>,and2a] by Th19;
x <> [<*(f . (n + 1)),(g . (n + 1))*>,'xor'] by A9, Th19;
hence ( not A = H₂(x,n) or for s being State of A holds Following (s,H₄(1)) is stable ) by A2, A10, Th25; :: thesis:

end;

set Sn = n -BitSubtracterStr (f,g);
set An = n -BitSubtracterCirc (f,g);
set o0 = 0 -BitBorrowOutput (f,g);
consider f1, g1, h1 being ManySortedSet of NAT such that
A11: n -BitSubtracterStr (f,g) = f1 . n and
A12: n -BitSubtracterCirc (f,g) = g1 . n and
A13: f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and
A14: g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and
A15: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and
A16: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f1 . n & A = g1 . n & z = h1 . n holds
( f1 . (n + 1) = S +* (BitSubtracterWithBorrowStr ((f . (n + 1)),(g . (n + 1)),z)) & g1 . (n + 1) = A +* (BitSubtracterWithBorrowCirc ((f . (n + 1)),(g . (n + 1)),z)) & h1 . (n + 1) = BorrowOutput ((f . (n + 1)),(g . (n + 1)),z) ) by Def2;

let i be object ; :: thesis:
assume i in NAT ; :: thesis:
then reconsider j = i as Element of NAT ;
thus h1 . i = j -BitBorrowOutput (f,g) by A13, A14, A15, A16, Th1
.= h . i by A6 ; :: thesis:

end;

then A17: h1 = h by PBOOLE:3;
A18: ex u, v being ManySortedSet of NAT st
( n -BitSubtracterStr (f,g) = u . H₄(2) & n -BitSubtracterCirc (f,g) = v . H₄(2) & u . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & v . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = 0 -BitBorrowOutput (f,g) & ( for n being Nat
for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over H₁(x,n) st S = u . n & A1 = v . n & x = h . n & A2 = H₂(x,n) holds
( u . (n + 1) = S +* H₁(x,n) & v . (n + 1) = A1 +* A2 & h . (n + 1) = H₃(x,n) ) ) )

take f1 ; :: thesis:
take g1 ; :: thesis:
thus ( n -BitSubtracterStr (f,g) = f1 . H₄(2) & n -BitSubtracterCirc (f,g) = g1 . H₄(2) & f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = 0 -BitBorrowOutput (f,g) & ( for n being Nat
for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over H₁(x,n) st S = f1 . n & A1 = g1 . n & x = h . n & A2 = H₂(x,n) holds
( f1 . (n + 1) = S +* H₁(x,n) & g1 . (n + 1) = A1 +* A2 & h . (n + 1) = H₃(x,n) ) ) ) by A3, A6, A11, A12, A13, A14, A16, A17; :: thesis:

end;

end;

A31: for n being Nat
for x being set st x = h . n holds
( h . (n + 1) = H₃(x,n) & x in InputVertices H₁(x,n) & H₃(x,n) in InnerVertices H₁(x,n) )

let n be Nat; :: thesis:
let x be set ; :: thesis:
assume A32: x = h . n ; :: thesis:
n in NAT by ORDINAL1:def 12;
then A33: x = n -BitBorrowOutput (f,g) by A6, A32;
h . (n + 1) = (n + 1) -BitBorrowOutput (f,g) by A6;
hence h . (n + 1) = H₃(x,n) by A33, Th7; :: thesis:
A34: x <> [<*(f . (n + 1)),(g . (n + 1))*>,and2a] by A33, Th19;
x <> [<*(f . (n + 1)),(g . (n + 1))*>,'xor'] by A33, Th19;
then InputVertices H₁(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A34, Th16;
hence x in InputVertices H₁(x,n) by ENUMSET1:def 1; :: thesis:
set xx = f . (n + 1);
set xy = g . (n + 1);
A35: H₃(x,n) in {H₃(x,n)} by TARSKI:def 1;
InnerVertices H₁(x,n) = ({[<*(f . (n + 1)),(g . (n + 1))*>,'xor'],(2GatesCircOutput ((f . (n + 1)),(g . (n + 1)),x,'xor'))} \/ {[<*(f . (n + 1)),(g . (n + 1))*>,and2a],[<*(g . (n + 1)),x*>,and2],[<*(f . (n + 1)),x*>,and2a]}) \/ {(BorrowOutput ((f . (n + 1)),(g . (n + 1)),x))} by Th17;
hence H₃(x,n) in InnerVertices H₁(x,n) by A35, XBOOLE_0:def 3; :: thesis:

end;