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 S₁[ Element of NAT ] means InnerVertices ($1 -BitAdderStr x,y) is Relation;
0 -BitAdderStr x,y = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) by Th8;
then A1: S₁[ 0 ] by FACIRC_1:38;
A2: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A3: InnerVertices (i -BitAdderStr x,y) is Relation ; :: thesis: S₁[i + 1]
A4: (i + 1) -BitAdderStr x,y = (i -BitAdderStr x,y) +* (BitAdderWithOverflowStr (x . (i + 1)),(y . (i + 1)),(i -BitMajorityOutput x,y)) by Th13;
InnerVertices (BitAdderWithOverflowStr (x . (i + 1)),(y . (i + 1)),(i -BitMajorityOutput x,y)) is Relation by FACIRC_1:88;
hence S₁[i + 1] by A3, A4, FACIRC_1:3; :: thesis: verum

end;

for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A1, A2);
hence InnerVertices (n -BitAdderStr x,y) is Relation ; :: thesis: verum