let n be Element of NAT ; for x, y being FinSequence holds InnerVertices (n -BitSubtracterStr (x,y)) is Relation
let x, y be FinSequence; InnerVertices (n -BitSubtracterStr (x,y)) is Relation
defpred S1[ Nat] means InnerVertices ($1 -BitSubtracterStr (x,y)) is Relation;
0 -BitSubtracterStr (x,y) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))
by Th2;
then A1:
S1[ 0 ]
by FACIRC_1:38;
A2:
now for i being Nat st S1[i] holds
S1[i + 1]let i be
Nat;
( S1[i] implies S1[i + 1] )assume A3:
S1[
i]
;
S1[i + 1]A4:
(i + 1) -BitSubtracterStr (
x,
y)
= (i -BitSubtracterStr (x,y)) +* (BitSubtracterWithBorrowStr ((x . (i + 1)),(y . (i + 1)),(i -BitBorrowOutput (x,y))))
by Th7;
InnerVertices (BitSubtracterWithBorrowStr ((x . (i + 1)),(y . (i + 1)),(i -BitBorrowOutput (x,y)))) is
Relation
by FSCIRC_1:22;
hence
S1[
i + 1]
by A3, A4, FACIRC_1:3;
verum end;
for i being Nat holds S1[i]
from NAT_1:sch 2(A1, A2);
hence
InnerVertices (n -BitSubtracterStr (x,y)) is Relation
; verum