let n be Element of NAT ; :: thesis: for x, y being FinSequence holds InnerVertices (n -BitAdderStr (x,y)) is Relation
let x, y be FinSequence; :: thesis: InnerVertices (n -BitAdderStr (x,y)) is Relation
defpred S1[ Nat] means InnerVertices ($1 -BitAdderStr (x,y)) is Relation;
0 -BitAdderStr (x,y) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) by Th7;
then A1: S1[ 0 ] by FACIRC_1:38;
A2: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A3: InnerVertices (i -BitAdderStr (x,y)) is Relation ; :: thesis: S1[i + 1]
A4: (i + 1) -BitAdderStr (x,y) = (i -BitAdderStr (x,y)) +* (BitAdderWithOverflowStr ((x . (i + 1)),(y . (i + 1)),(i -BitMajorityOutput (x,y)))) by Th12;
InnerVertices (BitAdderWithOverflowStr ((x . (i + 1)),(y . (i + 1)),(i -BitMajorityOutput (x,y)))) is Relation by FACIRC_1:88;
hence S1[i + 1] by A3, A4, FACIRC_1:3; :: thesis: verum
end;
for i being Nat holds S1[i] from NAT_1:sch 2(A1, A2);
 hence InnerVertices (n -BitAdderStr (x,y)) is Relation ; :: thesis: verum