let n be Element of NAT ; for x, y being FinSequence holds InnerVertices ((n + 1) -BitAdderStr (x,y)) = (InnerVertices (n -BitAdderStr (x,y))) \/ (InnerVertices (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y)))))
let x, y be FinSequence; InnerVertices ((n + 1) -BitAdderStr (x,y)) = (InnerVertices (n -BitAdderStr (x,y))) \/ (InnerVertices (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y)))))
(n + 1) -BitAdderStr (x,y) = (n -BitAdderStr (x,y)) +* (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y))))
by Th12;
hence
InnerVertices ((n + 1) -BitAdderStr (x,y)) = (InnerVertices (n -BitAdderStr (x,y))) \/ (InnerVertices (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y)))))
by FACIRC_1:27; verum