let f, g be nonpair-yielding FinSequence; :: thesis:
deffunc H₁( Nat) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign = $1 -BitSubtracterStr (f,g);
deffunc H₂( set , Nat) -> ManySortedSign = BitSubtracterWithBorrowStr ((f . ($2 + 1)),(g . ($2 + 1)),$1);
deffunc H₃( Nat) -> Element of InnerVertices ($1 -BitSubtracterStr (f,g)) = $1 -BitBorrowOutput (f,g);
consider h being ManySortedSet of NAT such that
A1: for n being Element of NAT holds h . n = H₃(n) from PBOOLE:sch 5();
A2: for n being Nat holds h . n = H₃(n)

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 12;
hence h . n = H₃(n) by A1; :: thesis:

end;

deffunc H₄( Nat) -> set = h . $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 k = (0 -tuples_on BOOLEAN) --> TRUE;
A3: 0 -BitSubtracterStr (f,g) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) by Th2;
then A4: InnerVertices H₁( 0 ) is Relation by FACIRC_1:38;
A5: InputVertices H₁( 0 ) is without_pairs by A3, FACIRC_1:39;
H₄( 0 ) = 0 -BitBorrowOutput (f,g) by A2;
then A6: h . 0 in InnerVertices H₁( 0 ) ;
A7: for n being Nat
for x being set holds InnerVertices H₂(x,n) is Relation by FSCIRC_1:22;

A8: now :: thesis:

let n be Element of NAT ; :: thesis:
let x be set ; :: thesis:
assume A9: x = H₄(n) ; :: thesis:
A10: H₄(n) = n -BitBorrowOutput (f,g) by A2;
then A11: x <> [<*(f . (n + 1)),(g . (n + 1))*>,and2a] by A9, Th19;
x <> [<*(f . (n + 1)),(g . (n + 1))*>,'xor'] by A9, A10, Th19;
hence InputVertices H₂(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A11, Th16; :: thesis:

end;

A12: for n being Nat
for x being set st x = h . n holds
(InputVertices H₂(x,n)) \ {x} is without_pairs

let n be Nat; :: thesis:
let x be set ; :: thesis:
assume A13: x = H₄(n) ; :: thesis:
n in NAT by ORDINAL1:def 12;
then A14: InputVertices H₂(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A8, A13;
thus (InputVertices H₂(x,n)) \ {x} is without_pairs :: thesis:

let a be pair object ; :: according to FACIRC_1:def 2 :: thesis:
assume A15: a in (InputVertices H₂(x,n)) \ {x} ; :: thesis:
then a in InputVertices H₂(x,n) by XBOOLE_0:def 5;
then A16: ( a = f . (n + 1) or a = g . (n + 1) or a = x ) by A14, ENUMSET1:def 1;
not a in {x} by A15, XBOOLE_0:def 5;
hence contradiction by A16, TARSKI:def 1; :: thesis:

end;

end;

A17: now :: thesis:

let n be Nat; :: thesis:
let S be non empty ManySortedSign ; :: thesis:
let x be set ; :: thesis:
A18: n in NAT by ORDINAL1:def 12;
assume that
A19: S = H₁(n) and
A20: x = h . n ; :: thesis:
A21: x = n -BitBorrowOutput (f,g) by A2, A20;
A22: H₄(n + 1) = (n + 1) -BitBorrowOutput (f,g) by A2;
thus H₁(n + 1) = S +* H₂(x,n) by A19, A21, Th7; :: thesis:
thus h . (n + 1) = H₅(x,n) by A21, A22, Th7; :: thesis:
InputVertices H₂(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A8, A18, A20;
hence x in InputVertices H₂(x,n) by ENUMSET1:def 1; :: thesis:
A23: 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;
H₅(x,n) in {H₅(x,n)} by TARSKI:def 1;
hence H₅(x,n) in InnerVertices H₂(x,n) by A23, XBOOLE_0:def 3; :: thesis:

end;

A24: for n being Nat holds
( InputVertices H₁(n + 1) = (InputVertices H₁(n)) \/ ((InputVertices H₂(h . n,n)) \ {(h . n)}) & InnerVertices H₁(n) is Relation & InputVertices H₁(n) is without_pairs ) from CIRCCMB2:sch 11(A4, A5, A6, A7, A12, A17);
let n be Nat; :: thesis:
h . n = n -BitBorrowOutput (f,g) by A2;
hence ( 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 ) by A24; :: thesis: