let n be Element of NAT ; :: thesis: 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; :: thesis: 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 Th13;
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; :: thesis: verum